nbn Show Code edit
# The negation of a wff is equivalent to the wff's equivalence to
# falsehood.
## Negated Proposition is equivalent to falsehood
thm (nbn () (nbn.1 (-. ph)) (<-> (-. ps) (<-> ps ph)) nbn.1 ph ps nbn2 ax-mp ph ps bicom bitri)
(<-> (-. ps) (<-> ps ph))
edit