pm2.86i Show Code edit
## Converse of ax-2
##
## pm2.86 written as an inference.
##
thm (pm2.86i () (1 (-> (-> ph ps) (-> ph ch))) (-> ph (-> ps ch))
1 himp1i com12)
(-> ph (-> ps ch))
edit