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