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