pm4.57 Show Code edit
# Theorem *4.57 of [bib/WhiteheadRussell] p. 120.
## Collary of DeMorgan's law
thm (pm4.57 () () (<-> (-. (/\ (-. ph) (-. ps))) (\/ ph ps)) ph ps oran bicomi)
(<-> (-. (/\ (-. ph) (-. ps))) (\/ ph ps))
edit