con2bid Show Code edit
## Contraposition
thm (con2bid () (con2bid.1 (-> ph (<-> ps (-. ch)))) (-> ph (<-> ch (-. ps))) con2bid.1 ch ps con2bi sylibr)
(-> ph (<-> ch (-. ps)))
edit