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 1569   ≠ 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  4612  nelprd  4614  eldifpr  4615  0nelop  5468  om00  8590  om00el  8591  oeoe  8615  mulne0b  11964  xmulpnf1  13411  lcmgcd  16791  lcmdvds  16792  domnmuln0  20970  isdomn3  20975  drngmulne0  21028  abvn0b  21102  lvecvsn0  21396  mdetralt  22932  ply1domn  26451  vieta1lem1  26642  vieta1lem2  26643  atandm  27213  atandm3  27215  dchrelbas3  27574  mulsne0bd  28581  eupth2lem3lem7  30844  frgrreg  31004  nmlno0lem  31404  nmlnop0iALT  32606  chirredi  33005  nelpr  33178  minplyirred  34393  subfacp1lem1  36034  filnetlem4  37265  disjecxrn  39453  lcvbr3  40189  cvrnbtwn4  40445  elpadd0  40975  cdleme0moN  41391  cdleme0nex  41456  mulltgt0d  43655  mullt0b2d  43657  sn-mullt0d  43658  fsuppind  43727  lidldomnnring  49441