con2 Show Code edit
## Contraposition
thm (con2 () () (-> (-> ph (-. ps)) (-> ps (-. ph)))
ph dn (-. ps) imim1i (-. ph) ps ax-3 syl)
(-> (-> ph (-. ps)) (-> ps (-. ph)))
edit