Theorem ianor

Negated conjunction in terms of disjunction (De Morgan's law). Theorem *4.51 of [WhiteheadRussell] p. 120. (Contributed by NM, 14-May-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.)

Conclusion
\( \vdash \neg (\varphi \wedge \psi) \leftrightarrow \neg \varphi \vee \neg \psi \)
Proof
l0
imnan
\( \vdash \varphi \rightarrow \neg \psi \leftrightarrow \neg (\varphi \wedge \psi) \)
pm4.62
\( \vdash \varphi \rightarrow \neg \psi \leftrightarrow \neg \varphi \vee \neg \psi \)
bitr3i l0 _