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