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