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