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