Theorem 3pm3.2ni

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

	Ref	Expression
Hypotheses	3pm3.2ni.1	⊢ ¬ 𝜑
	3pm3.2ni.2	⊢ ¬ 𝜓
	3pm3.2ni.3	⊢ ¬ 𝜒
Assertion	3pm3.2ni	⊢ ¬ ( 𝜑 ∨ 𝜓 ∨ 𝜒 )

Proof

Step	Hyp	Ref	Expression
1		3pm3.2ni.1	⊢ ¬ 𝜑
2		3pm3.2ni.2	⊢ ¬ 𝜓
3		3pm3.2ni.3	⊢ ¬ 𝜒
4	1 2	pm3.2ni	⊢ ¬ ( 𝜑 ∨ 𝜓 )
5	4 3	pm3.2ni	⊢ ¬ ( ( 𝜑 ∨ 𝜓 ) ∨ 𝜒 )
6		df-3or	⊢ ( ( 𝜑 ∨ 𝜓 ∨ 𝜒 ) ↔ ( ( 𝜑 ∨ 𝜓 ) ∨ 𝜒 ) )
7	5 6	mtbir	⊢ ¬ ( 𝜑 ∨ 𝜓 ∨ 𝜒 )