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