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