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