Theorem 3ianor

Negated triple conjunction expressed in terms of triple disjunction. (Contributed by Jeff Hankins, 15-Aug-2009.) (Proof shortened by Andrew Salmon, 13-May-2011.) Shorten with xchnxbir. (Revised by Wolf Lammen, 8-Apr-2022.)

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