pm3.1 Show Code edit
# Theorem *3.1 of [bib/WhiteheadRussell] p. 111.
## Collary of DeMorgan's law
thm (pm3.1 () () (-> (/\ ph ps) (-. (\/ (-. ph) (-. ps)))) ph ps anor biimpi)
(-> (/\ ph ps) (-. (\/ (-. ph) (-. ps))))
edit