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