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