Theorem 3ioran

Negated triple disjunction as triple conjunction. (Contributed by Scott Fenton, 19-Apr-2011.)

Conclusion
\( \vdash \neg (\varphi \vee \psi \vee \chi) \leftrightarrow \neg \varphi \wedge \neg \psi \wedge \neg \chi \)
Proof
ioran
l1
anbi1i _
\( \vdash \neg (\varphi \vee \psi) \wedge \neg \chi \leftrightarrow \neg \varphi \wedge \neg \psi \wedge \neg \chi \)
l2
ioran
\( \vdash \neg (\varphi \vee \psi \vee \chi) \leftrightarrow \neg (\varphi \vee \psi) \wedge \neg \chi \)
df-3or
\( \vdash \varphi \vee \psi \vee \chi \leftrightarrow \varphi \vee \psi \vee \chi \)
l4
xchnxbir l2 _
\( \vdash \neg (\varphi \vee \psi \vee \chi) \leftrightarrow \neg (\varphi \vee \psi) \wedge \neg \chi \)
df-3an
\( \vdash \neg \varphi \wedge \neg \psi \wedge \neg \chi \leftrightarrow \neg \varphi \wedge \neg \psi \wedge \neg \chi \)
3bitr4i l1 l4 _