Metamath Proof Explorer

Theorem 3ioran

Description: Negated triple disjunction as triple conjunction. (Contributed by Scott Fenton, 19-Apr-2011)

Ref Expression
Assertion 3ioran ⊢ ¬ φ ∨ ψ ∨ χ ↔ ¬ φ ∧ ¬ ψ ∧ ¬ χ

Proof

Step Hyp Ref Expression
1 ioran ⊢ ¬ φ ∨ ψ ↔ ¬ φ ∧ ¬ ψ
2 1 anbi1i ⊢ ¬ φ ∨ ψ ∧ ¬ χ ↔ ¬ φ ∧ ¬ ψ ∧ ¬ χ
3 ioran ⊢ ¬ φ ∨ ψ ∨ χ ↔ ¬ φ ∨ ψ ∧ ¬ χ
4 df-3or ⊢ φ ∨ ψ ∨ χ ↔ φ ∨ ψ ∨ χ
5 3 4 xchnxbir ⊢ ¬ φ ∨ ψ ∨ χ ↔ ¬ φ ∨ ψ ∧ ¬ χ
6 df-3an ⊢ ¬ φ ∧ ¬ ψ ∧ ¬ χ ↔ ¬ φ ∧ ¬ ψ ∧ ¬ χ
7 2 5 6 3bitr4i ⊢ ¬ φ ∨ ψ ∨ χ ↔ ¬ φ ∧ ¬ ψ ∧ ¬ χ