con1 Show Code edit
## Contraposition
thm (con1 () () (-> (-> (-. ph) ps) (-> (-. ps) ph))
ps dnr (-. ph) imim2i ph (-. ps) ax-3 syl)
(-> (-> (-. ph) ps) (-> (-. ps) ph))
edit