con3 Show Code edit
## Contraposition
thm (con3 () () (-> (-> ph ps) (-> (-. ps) (-. ph)))
ph dn ps imim1i (-. ph) ps con1 syl)
(-> (-> ph ps) (-> (-. ps) (-. ph)))
edit