ad2antll Show Code edit
# Deduction adding conjuncts to antecedent.
## Add Conjuncts
thm (ad2antll () (ad2ant.1 (-> ph ps)) (-> (/\ ch (/\ th ph)) ps) ad2ant.1 th adantl ch adantl)
(-> (/\ ch (/\ th ph)) ps)
edit