Theorem neanior 3048

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

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   ∧ wa 401   ∨ wo 861   = wceq 1570   ≠ wne 2955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ne 2956

This theorem is used by:  nelpri  4616  nelprd  4618  eldifpr  4619  0nelop  5473  om00  8562  om00el  8563  oeoe  8587  mulne0b  11879  xmulpnf1  13326  lcmgcd  16697  lcmdvds  16698  domnmuln0  20871  isdomn3  20876  drngmulne0  20928  abvn0b  21002  lvecvsn0  21296  mdetralt  22830  ply1domn  26349  vieta1lem1  26542  vieta1lem2  26543  atandm  27113  atandm3  27115  dchrelbas3  27474  mulsne0bd  28451  eupth2lem3lem7  30714  frgrreg  30874  nmlno0lem  31274  nmlnop0iALT  32476  chirredi  32875  nelpr  33006  minplyirred  34221  subfacp1lem1  35758  filnetlem4  37000  disjecxrn  39160  lcvbr3  39896  cvrnbtwn4  40152  elpadd0  40682  cdleme0moN  41098  cdleme0nex  41163  mulltgt0d  43370  mullt0b2d  43372  sn-mullt0d  43373  fsuppind  43436  lidldomnnring  49151