pm2.86d Show Code edit
## Converse of ax-2
##
## pm2.86 written as an deduction.
##
thm (pm2.86d () (1 (-> ph (-> (-> ps ch) (-> ps th))))
(-> ph (-> ps (-> ch th)))
1 ps ch th pm2.86 syl)
(-> ph (-> ps (-> ch th)))
edit