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