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