con1b Show Code edit
## Contraposition
## Bidirectional version of con1.
thm (con1b () () (<-> (-> (-. ph) ps) (-> (-. ps) ph))
ph ps con1
(-> (-> (-. ph) ps) (-> (-. ps) ph))
ps ph con1
(-> (-> (-. ps) ph) (-> (-. ph) ps))
impbii)
(<-> (-> (-. ph) ps) (-> (-. ps) ph))
edit