3ad2antr2 Show Code edit
# Deduction adding a conjuncts to antecedent.
thm (3ad2antr2 () (3ad2antl.1 (-> (/\ ph ch) th)) (-> (/\ ph (/\/\ ps ch ta)) th) 3ad2antl.1 ps adantrl ta 3adantr3)
(-> (/\ ph (/\/\ ps ch ta)) th)
edit