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