adantrll Show Code edit
# Deduction adding a conjunct to antecedent.
## Add Conjunct
thm (adantrll () (adantr2.1 (-> (/\ ph (/\ ps ch)) th)) (-> (/\ ph (/\ (/\ ta ps) ch)) th) adantr2.1 exp32 ta a1d imp44)
(-> (/\ ph (/\ (/\ ta ps) ch)) th)
edit