notbi Show Code edit
# Contraposition. Theorem *4.11 of [bib/WhiteheadRussell] p. 117.
## Negate Both Sides
## left('Simplify', '¬') right('Add', '¬')
thm (notbi () () (<-> (<-> ph ps) (<-> (-. ph) (-. ps))) ph ps con34b ps ph con34b anbi12i ph ps dfbi2 (-. ps) (-. ph) dfbi2 3bitr4i (-. ps) (-. ph) bicom bitri)
(<-> (<-> ph ps) (<-> (-. ph) (-. ps)))
edit