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