ianor Show Code edit
# Negated conjunction in terms of disjunction (DeMorgan's law). Theorem
# *4.51 of [bib/WhiteheadRussell] p. 120.
## DeMorgan's law
##
## De Morgan's law
## describing conjunction in terms of disjunction. For the non-negated form see
## anor.
##
thm (ianor () () (<-> (-. (/\ ph ps)) (\/ (-. ph) (-. ps))) ph ps anor notbii (\/ (-. ph) (-. ps)) notnot bitr4i)
(<-> (-. (/\ ph ps)) (\/ (-. ph) (-. ps)))
edit