Theorem neanior 3029

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 2935	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		df-ne 2935	. . 3 ⊢ (𝐶 ≠ 𝐷 ↔ ¬ 𝐶 = 𝐷)
3	1, 2	anbi12i 626	. 2 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷) ↔ (¬ 𝐴 = 𝐵 ∧ ¬ 𝐶 = 𝐷))
4		pm4.56 985	. 2 ⊢ ((¬ 𝐴 = 𝐵 ∧ ¬ 𝐶 = 𝐷) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷))
5	3, 4	bitri 275	1 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷))

Syntax hints:  ¬ wn 3   ↔ wb 205   ∧ wa 395   ∨ wo 844   = wceq 1533   ≠ wne 2934

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 206  df-an 396  df-or 845  df-ne 2935

This theorem is referenced by:  nelpri  4652  nelprd  4654  eldifpr  4655  0nelop  5489  om00  8576  om00el  8577  oeoe  8600  mulne0b  11859  xmulpnf1  13259  lcmgcd  16551  lcmdvds  16552  drngmulne0  20617  lvecvsn0  20960  domnmuln0  21208  abvn0b  21214  mdetralt  22465  ply1domn  26014  vieta1lem1  26200  vieta1lem2  26201  atandm  26763  atandm3  26765  dchrelbas3  27126  mulsne0bd  28041  eupth2lem3lem7  29996  frgrreg  30156  nmlno0lem  30555  nmlnop0iALT  31757  chirredi  32156  nelpr  32277  minplyirred  33290  subfacp1lem1  34698  filnetlem4  35774  disjecxrn  37772  lcvbr3  38406  cvrnbtwn4  38662  elpadd0  39193  cdleme0moN  39609  cdleme0nex  39674  fsuppind  41724  isdomn3  42528  lidldomnnring  47191