com12 Show Code edit
## Commute First and Second Antecedents
##
## (-> ph (-> ps ch))
## (-> ps (-> ph ch))
##
thm (com12 () (1 (-> ph (-> ps ch))) (-> ps (-> ph ch))
ps ph ax-1 1 a2i syl)
(-> ps (-> ph ch))
edit