con2i Show Code edit
## Contraposition
##
## (-> ph (-. ps))
## (-> ps (-. ph))
##
thm (con2i () (1 (-> ph (-. ps))) (-> ps (-. ph))
1 ph ps con2 ax-mp)
(-> ps (-. ph))
edit