pm2.04 Show Code edit
# aka com12t
## Commute First and Second Antecedents
##
## One line version of com12.
##
##
## (-> (-> ph (-> ps ch)) (-> ps (-> ph ch)))
##
thm (pm2.04 () () (-> (-> ph (-> ps ch)) (-> ps (-> ph ch)))
ph ps ch ax-2 ps ph ax-1 syl5)
(-> (-> ph (-> ps ch)) (-> ps (-> ph ch)))
edit