Theorem ne3anior

Description: A De Morgan's law for inequality. (Contributed by NM, 30-Sep-2013)

	Ref	Expression
Assertion	ne3anior	⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷 ∧ 𝐸 ≠ 𝐹 ) ↔ ¬ ( 𝐴 = 𝐵 ∨ 𝐶 = 𝐷 ∨ 𝐸 = 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		3anor	⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷 ∧ 𝐸 ≠ 𝐹 ) ↔ ¬ ( ¬ 𝐴 ≠ 𝐵 ∨ ¬ 𝐶 ≠ 𝐷 ∨ ¬ 𝐸 ≠ 𝐹 ) )
2		nne	⊢ ( ¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵 )
3		nne	⊢ ( ¬ 𝐶 ≠ 𝐷 ↔ 𝐶 = 𝐷 )
4		nne	⊢ ( ¬ 𝐸 ≠ 𝐹 ↔ 𝐸 = 𝐹 )
5	2 3 4	3orbi123i	⊢ ( ( ¬ 𝐴 ≠ 𝐵 ∨ ¬ 𝐶 ≠ 𝐷 ∨ ¬ 𝐸 ≠ 𝐹 ) ↔ ( 𝐴 = 𝐵 ∨ 𝐶 = 𝐷 ∨ 𝐸 = 𝐹 ) )
6	1 5	xchbinx	⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷 ∧ 𝐸 ≠ 𝐹 ) ↔ ¬ ( 𝐴 = 𝐵 ∨ 𝐶 = 𝐷 ∨ 𝐸 = 𝐹 ) )