Metamath Proof Explorer

Theorem 3ianor

Description: Negated triple conjunction expressed in terms of triple disjunction. (Contributed by Jeff Hankins, 15-Aug-2009) (Proof shortened by Andrew Salmon, 13-May-2011) Shorten with xchnxbir . (Revised by Wolf Lammen, 8-Apr-2022)

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

Proof

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