Theorem neanior 3036

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

Syntax hints:  ¬ wn 3   ↔ wb 205   ∧ wa 395   ∨ wo 843   = wceq 1539   ≠ wne 2942

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 206  df-an 396  df-or 844  df-ne 2943

This theorem is referenced by:  nelpri  4587  nelprd  4589  eldifpr  4590  0nelop  5404  om00  8368  om00el  8369  oeoe  8392  mulne0b  11546  xmulpnf1  12937  lcmgcd  16240  lcmdvds  16241  drngmulne0  19928  lvecvsn0  20286  domnmuln0  20482  abvn0b  20486  mdetralt  21665  ply1domn  25193  vieta1lem1  25375  vieta1lem2  25376  atandm  25931  atandm3  25933  dchrelbas3  26291  eupth2lem3lem7  28499  frgrreg  28659  nmlno0lem  29056  nmlnop0iALT  30258  chirredi  30657  nelpr  30780  subfacp1lem1  33041  filnetlem4  34497  lcvbr3  36964  cvrnbtwn4  37220  elpadd0  37750  cdleme0moN  38166  cdleme0nex  38231  fsuppind  40202  isdomn3  40945  lidldomnnring  45376