Theorem neanior 3109

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

Assertion

Ref	Expression
neanior	⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷))

Proof of Theorem neanior

Step	Hyp	Ref	Expression
1		df-ne 3017	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		df-ne 3017	. . 3 ⊢ (𝐶 ≠ 𝐷 ↔ ¬ 𝐶 = 𝐷)
3	1, 2	anbi12i 628	. 2 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷) ↔ (¬ 𝐴 = 𝐵 ∧ ¬ 𝐶 = 𝐷))
4		pm4.56 985	. 2 ⊢ ((¬ 𝐴 = 𝐵 ∧ ¬ 𝐶 = 𝐷) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷))
5	3, 4	bitri 277	1 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷))

Syntax hints:  ¬ wn 3   ↔ wb 208   ∧ wa 398   ∨ wo 843   = wceq 1537   ≠ wne 3016

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ne 3017

This theorem is referenced by:  nelpri  4594  nelprd  4596  eldifpr  4597  0nelop  5386  om00  8201  om00el  8202  oeoe  8225  mulne0b  11281  xmulpnf1  12668  lcmgcd  15951  lcmdvds  15952  drngmulne0  19524  lvecvsn0  19881  domnmuln0  20071  abvn0b  20075  mdetralt  21217  ply1domn  24717  vieta1lem1  24899  vieta1lem2  24900  atandm  25454  atandm3  25456  dchrelbas3  25814  eupth2lem3lem7  28013  frgrreg  28173  nmlno0lem  28570  nmlnop0iALT  29772  chirredi  30171  nelpr  30291  subfacp1lem1  32426  filnetlem4  33729  lcvbr3  36174  cvrnbtwn4  36430  elpadd0  36960  cdleme0moN  37376  cdleme0nex  37441  isdomn3  39824  lidldomnnring  44221