con1bii Show Code edit
## Contraposition
thm (con1bii () (1 (<-> (-. ph) ps)) (<-> (-. ps) ph)
1 biimpi
(-> (-. ph) ps)
con1i
(-> (-. ps) ph)
1 biimpri
(-> ps (-. ph))
con2i
(-> ph (-. ps))
impbii
(<-> (-. ps) ph)
)
edit