Theorem 3pm3.2ni

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

	Ref	Expression
Hypotheses	3pm3.2ni.1	$$⊢\neg \phi$$
	3pm3.2ni.2	$$⊢\neg \psi$$
	3pm3.2ni.3	$$⊢\neg \chi$$
Assertion	3pm3.2ni	$$⊢\neg \left(\phi \vee \psi \vee \chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		3pm3.2ni.1	$$⊢\neg \phi$$
2		3pm3.2ni.2	$$⊢\neg \psi$$
3		3pm3.2ni.3	$$⊢\neg \chi$$
4	1 2	pm3.2ni	$$⊢\neg \left(\phi \vee \psi \right)$$
5	4 3	pm3.2ni	$$⊢\neg \left(\left(\phi \vee \psi \right)\vee \chi \right)$$
6		df-3or	$$⊢\left(\phi \vee \psi \vee \chi \right)\leftrightarrow \left(\left(\phi \vee \psi \right)\vee \chi \right)$$
7	5 6	mtbir	$$⊢\neg \left(\phi \vee \psi \vee \chi \right)$$