Theorem neanior 3049

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

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 2957

This theorem is used by:  nelpri  4616  nelprd  4618  eldifpr  4619  0nelop  5468  om00  8576  om00el  8577  oeoe  8601  mulne0b  11950  xmulpnf1  13397  lcmgcd  16775  lcmdvds  16776  domnmuln0  20954  isdomn3  20959  drngmulne0  21012  abvn0b  21086  lvecvsn0  21380  mdetralt  22916  ply1domn  26435  vieta1lem1  26626  vieta1lem2  26627  atandm  27197  atandm3  27199  dchrelbas3  27558  mulsne0bd  28565  eupth2lem3lem7  30828  frgrreg  30988  nmlno0lem  31388  nmlnop0iALT  32590  chirredi  32989  nelpr  33120  minplyirred  34336  subfacp1lem1  35923  filnetlem4  37149  disjecxrn  39324  lcvbr3  40060  cvrnbtwn4  40316  elpadd0  40846  cdleme0moN  41262  cdleme0nex  41327  mulltgt0d  43526  mullt0b2d  43528  sn-mullt0d  43529  fsuppind  43598  lidldomnnring  49302