nbbn Show Code edit
# Move negation outside of biconditional. Compare Theorem *5.18 of
# [bib/WhiteheadRussell] p. 124.
## Move negation outside biconditional
thm (nbbn () () (<-> (<-> (-. ph) ps) (-. (<-> ph ps))) (-. ph) ps bicom ph ps bicom ps ph pm5.18 bitri con2bii bitri)
(<-> (<-> (-. ph) ps) (-. (<-> ph ps)))
edit