Theorem ioran

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

Conclusion
\( \vdash \neg (\varphi \vee \psi) \leftrightarrow \neg \varphi \wedge \neg \psi \)
Proof
l0
pm4.65
\( \vdash \neg (\neg \varphi \rightarrow \psi) \leftrightarrow \neg \varphi \wedge \neg \psi \)
pm4.64
\( \vdash \neg \varphi \rightarrow \psi \leftrightarrow \varphi \vee \psi \)
xchnxbi l0 _