anc2li Show Code edit
# Deduction conjoining antecedent to left of consequent in nested
# implication.
## Add Antecedent
thm (anc2li () (anc2li.1 (-> ph (-> ps ch))) (-> ph (-> ps (/\ ph ch))) anc2li.1 ph ps ch anc2l ax-mp)
(-> ph (-> ps (/\ ph ch)))
edit