anc2l Show Code edit
# Conjoin antecedent to left of consequent in nested implication.
## Add Antecedent
thm (anc2l () () (-> (-> ph (-> ps ch)) (-> ph (-> ps (/\ ph ch)))) ph ch pm3.2 ps imim2d a2i)
(-> (-> ph (-> ps ch)) (-> ph (-> ps (/\ ph ch))))
edit