Theorem neanior 3027

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 634	. 2 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷) ↔ (¬ 𝐴 = 𝐵 ∧ ¬ 𝐶 = 𝐷))
4		pm4.56 996	. 2 ⊢ ((¬ 𝐴 = 𝐵 ∧ ¬ 𝐶 = 𝐷) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷))
5	3, 4	bitri 276	1 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷))

Syntax hints:  ¬ wn 3   ↔ wb 207   ∧ wa 396   ∨ wo 853   = wceq 1547   ≠ 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 208  df-an 397  df-or 854  df-ne 2935

This theorem is referenced by:  nelpri  4587  nelprd  4589  eldifpr  4590  0nelop  5437  om00  8500  om00el  8501  oeoe  8525  mulne0b  11782  xmulpnf1  13217  lcmgcd  16567  lcmdvds  16568  domnmuln0  20681  isdomn3  20687  drngmulne0  20734  abvn0b  20808  lvecvsn0  21102  mdetralt  22591  ply1domn  26107  vieta1lem1  26294  vieta1lem2  26295  atandm  26858  atandm3  26860  dchrelbas3  27219  mulsne0bd  28196  eupth2lem3lem7  30322  frgrreg  30482  nmlno0lem  30882  nmlnop0iALT  32084  chirredi  32483  nelpr  32619  minplyirred  33895  subfacp1lem1  35407  filnetlem4  36609  disjecxrn  38779  lcvbr3  39515  cvrnbtwn4  39771  elpadd0  40301  cdleme0moN  40717  cdleme0nex  40782  mulltgt0d  42972  mullt0b2d  42974  sn-mullt0d  42975  fsuppind  43040  lidldomnnring  48727