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