pm2.86 Show Code edit
## Converse of ax-2
thm (pm2.86 () () (-> (-> (-> ph ps) (-> ph ch)) (-> ph (-> ps ch)))
ph ps (-> ph ch) himp1 com23)
(-> (-> (-> ph ps) (-> ph ch)) (-> ph (-> ps ch)))
edit