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