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

Metamath Proof Explorer

Theorem neanior

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

Ref Expression
Assertion neanior ⊢ 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 anbi12i ⊢ A ≠ B ∧ C ≠ D ↔ ¬ A = B ∧ ¬ C = D
4 pm4.56 ⊢ ¬ A = B ∧ ¬ C = D ↔ ¬ A = B ∨ C = D
5 3 4 bitri ⊢ A ≠ B ∧ C ≠ D ↔ ¬ A = B ∨ C = D