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

Metamath Proof Explorer

Theorem neorian

Description: A De Morgan's law for inequality. (Contributed by NM, 18-May-2007)

Ref Expression
Assertion neorian ⊢ A ≠ B ∨ C ≠ D ↔ ¬ A = B ∧ C = D

Proof

Step Hyp Ref Expression
1 df-ne ⊢ A ≠ B ↔ ¬ A = B
2 df-ne ⊢ C ≠ D ↔ ¬ C = D
3 1 2 orbi12i ⊢ A ≠ B ∨ C ≠ D ↔ ¬ A = B ∨ ¬ C = D
4 ianor ⊢ ¬ A = B ∧ C = D ↔ ¬ A = B ∨ ¬ C = D
5 3 4 bitr4i ⊢ A ≠ B ∨ C ≠ D ↔ ¬ A = B ∧ C = D