Theorem anor

Conjunction in terms of disjunction (De Morgan's law). Theorem *4.5 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 3-Nov-2012.)

Conclusion
\( \vdash \varphi \wedge \psi \leftrightarrow \neg (\neg \varphi \vee \neg \psi) \)
Proof
l0
notnotb
\( \vdash \varphi \wedge \psi \leftrightarrow \neg \neg (\varphi \wedge \psi) \)
ianor
\( \vdash \neg (\varphi \wedge \psi) \leftrightarrow \neg \varphi \vee \neg \psi \)
xchbinx l0 _