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