3adant3r1 Show Code edit
# Deduction adding a conjunct to antecedent.
thm (3adant3r1 () (3exp.1 (-> (/\/\ ph ps ch) th)) (-> (/\ ph (/\/\ ta ps ch)) th) 3exp.1 3expb ta 3adantr1)
(-> (/\ ph (/\/\ ta ps ch)) th)
edit