3ad2antl1 Show Code edit
# Deduction adding conjuncts to antecedent.
thm (3ad2antl1 () (3ad2antl.1 (-> (/\ ph ch) th)) (-> (/\ (/\/\ ph ps ta) ch) th) 3ad2antl.1 ta adantlr ps 3adantl2)
(-> (/\ (/\/\ ph ps ta) ch) th)
edit