anor Show Code edit
# Conjunction in terms of disjunction (DeMorgan's law). Theorem *4.5 of
# [bib/WhiteheadRussell] p. 120.
## DeMorgan's law
##
## De Morgan's law
## describing conjunction in terms of disjunction. For an alternative form see
## oran.
##
thm (anor () () (<-> (/\ ph ps) (-. (\/ (-. ph) (-. ps)))) ph ps df-an ph ps pm4.62 notbii bitri)
(<-> (/\ ph ps) (-. (\/ (-. ph) (-. ps))))
edit