Theorem neanior 3052

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 2960	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		df-ne 2960	. . 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 2959

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 2960

This theorem is used by:  nelpr  4614  nelpri  4617  nelprd  4619  eldifpr  4620  0nelop  5475  om00  8621  om00el  8622  oeoe  8646  mulne0b  11997  xmulpnf1  13444  lcmgcd  16826  lcmdvds  16827  domnmuln0  21012  isdomn3  21017  drngmulne0  21070  abvn0b  21144  lvecvsn0  21438  mdetralt  22978  ply1domn  26497  vieta1lem1  26688  vieta1lem2  26689  atandm  27261  atandm3  27263  dchrelbas3  27622  mulsne0bd  28629  eupth2lem3lem7  30892  frgrreg  31052  nmlno0lem  31452  nmlnop0iALT  32654  chirredi  33053  minplyirred  34454  subfacp1lem1  36152  filnetlem4  37384  disjecxrn  39610  lcvbr3  40346  cvrnbtwn4  40602  elpadd0  41132  cdleme0moN  41548  cdleme0nex  41613  mulltgt0d  43812  mullt0b2d  43814  sn-mullt0d  43815  fsuppind  43884  lidldomnnring  49606