adantrr Show Code edit
# Deduction adding a conjunct to antecedent.
## Add Conjunct
thm (adantrr () (adant2.1 (-> (/\ ph ps) ch)) (-> (/\ ph (/\ ps th)) ch) adant2.1 ex th adantrd imp)
(-> (/\ ph (/\ ps th)) ch)
edit