Theorem pm4.56

Theorem *4.56 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)

Conclusion
\( \vdash \neg \varphi \wedge \neg \psi \leftrightarrow \neg (\varphi \vee \psi) \)
Proof
ioran
bicomi _