Theorem 3pm3.2ni

Triple negated disjunction introduction. (Contributed by Scott Fenton, 20-Apr-2011.)

Hypotheses
3pm3.2ni.1
\( \vdash \neg \varphi \)
3pm3.2ni.2
\( \vdash \neg \psi \)
3pm3.2ni.3
\( \vdash \neg \chi \)
Conclusion
\( \vdash \neg (\varphi \vee \psi \vee \chi) \)
Proof
l0
3pm3.2ni.1
3pm3.2ni.2
l2
pm3.2ni l0 _
3pm3.2ni.3
l4
pm3.2ni l2 _
\( \vdash \neg (\varphi \vee \psi \vee \chi) \)
df-3or
\( \vdash \varphi \vee \psi \vee \chi \leftrightarrow \varphi \vee \psi \vee \chi \)
mtbir l4 _