Theorem 3ioran 950

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

Assertion

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

Proof of Theorem 3ioran

Step	Hyp	Ref	Expression
1		ioran 476	. . 3 ⊢ (¬ (φ ∨ ψ) ↔ (¬ φ ∧ ¬ ψ))
2	1	anbi1i 676	. 2 ⊢ ((¬ (φ ∨ ψ) ∧ ¬ χ) ↔ ((¬ φ ∧ ¬ ψ) ∧ ¬ χ))
3		ioran 476	. . 3 ⊢ (¬ ((φ ∨ ψ) ∨ χ) ↔ (¬ (φ ∨ ψ) ∧ ¬ χ))
4		df-3or 935	. . 3 ⊢ ((φ ∨ ψ ∨ χ) ↔ ((φ ∨ ψ) ∨ χ))
5	3, 4	xchnxbir 300	. 2 ⊢ (¬ (φ ∨ ψ ∨ χ) ↔ (¬ (φ ∨ ψ) ∧ ¬ χ))
6		df-3an 936	. 2 ⊢ ((¬ φ ∧ ¬ ψ ∧ ¬ χ) ↔ ((¬ φ ∧ ¬ ψ) ∧ ¬ χ))
7	2, 5, 6	3bitr4i 268	1 ⊢ (¬ (φ ∨ ψ ∨ χ) ↔ (¬ φ ∧ ¬ ψ ∧ ¬ χ))

Syntax hints:  ¬ wn 3   ↔ wb 176   ∨ wo 357   ∧ wa 358   ∨ w3o 933   ∧ w3a 934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936

This theorem is referenced by:  3oran  951  cadnot  1394