Theorem 3ioran 939

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 704	. . 3 ⊢ (¬ (𝜑 ∨ 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))
2	1	anbi1i 446	. 2 ⊢ ((¬ (𝜑 ∨ 𝜓) ∧ ¬ 𝜒) ↔ ((¬ 𝜑 ∧ ¬ 𝜓) ∧ ¬ 𝜒))
3		ioran 704	. . 3 ⊢ (¬ ((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (¬ (𝜑 ∨ 𝜓) ∧ ¬ 𝜒))
4		df-3or 925	. . 3 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒))
5	3, 4	xchnxbir 641	. 2 ⊢ (¬ (𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (¬ (𝜑 ∨ 𝜓) ∧ ¬ 𝜒))
6		df-3an 926	. 2 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓 ∧ ¬ 𝜒) ↔ ((¬ 𝜑 ∧ ¬ 𝜓) ∧ ¬ 𝜒))
7	2, 5, 6	3bitr4i 210	1 ⊢ (¬ (𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (¬ 𝜑 ∧ ¬ 𝜓 ∧ ¬ 𝜒))

Syntax hints:  ¬ wn 3   ∧ wa 102   ↔ wb 103   ∨ wo 664   ∨ w3o 923   ∧ w3a 924

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 579  ax-in2 580  ax-io 665

This theorem depends on definitions:  df-bi 115  df-3or 925  df-3an 926

This theorem is referenced by:  ne3anior  2343