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