adantrd Show Code edit
# Deduction adding a conjunct to the right of an antecedent.
## Add Conjunct
thm (adantrd () (adantrd.1 (-> ph (-> ps ch))) (-> ph (-> (/\ ps th) ch)) adantrd.1 ps th pm3.26 syl5)
(-> ph (-> (/\ ps th) ch))
edit