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