This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ne3anior

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

Ref Expression
Assertion ne3anior ⊢ A ≠ B ∧ C ≠ D ∧ E ≠ F ↔ ¬ A = B ∨ C = D ∨ E = F

Proof

Step Hyp Ref Expression
1 3anor ⊢ A ≠ B ∧ C ≠ D ∧ E ≠ F ↔ ¬ ¬ A ≠ B ∨ ¬ C ≠ D ∨ ¬ E ≠ F
2 nne ⊢ ¬ A ≠ B ↔ A = B
3 nne ⊢ ¬ C ≠ D ↔ C = D
4 nne ⊢ ¬ E ≠ F ↔ E = F
5 2 3 4 3orbi123i ⊢ ¬ A ≠ B ∨ ¬ C ≠ D ∨ ¬ E ≠ F ↔ A = B ∨ C = D ∨ E = F
6 1 5 xchbinx ⊢ A ≠ B ∧ C ≠ D ∧ E ≠ F ↔ ¬ A = B ∨ C = D ∨ E = F