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