com23 Show Code edit
## Commute Second and Third Antecedents
##
## (-> ph (-> ps (-> ch th)))
## (-> ph (-> ch (-> ps th)))
##
thm (com23 () (1 (-> ph (-> ps (-> ch th)))) (-> ph (-> ch (-> ps th)))
1 ps ch th pm2.04 syl)
(-> ph (-> ch (-> ps th)))
edit