adantld Show Code edit
# Deduction adding a conjunct to the left of an antecedent.
## Add Conjunct
thm (adantld () (adantld.1 (-> ph (-> ps ch))) (-> ph (-> (/\ th ps) ch)) adantld.1 th a1d imp3a)
(-> ph (-> (/\ th ps) ch))
edit