3adantl2 Show Code edit
# Deduction adding a conjunct to antecedent.
thm (3adantl2 () (3adantl.1 (-> (/\ (/\ ph ps) ch) th)) (-> (/\ (/\/\ ph ta ps) ch) th) 3adantl.1 ex ta 3adant2 imp)
(-> (/\ (/\/\ ph ta ps) ch) th)
edit