con3d Show Code edit
## Contraposition
thm (con3d () (1 (-> ph (-> ps ch))) (-> ph (-> (-. ch) (-. ps)))
1 ps ch con3 syl)
(-> ph (-> (-. ch) (-. ps)))
edit