This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ¬ ( 𝜑 ∨ 𝜓 ∨ 𝜒 )