Theorem neanior 3057

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

Syntax hints:  ¬ wn 3   ↔ wb 209   ∧ wa 400   ∨ wo 860   = wceq 1567   ≠ wne 2964

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 210  df-an 401  df-or 861  df-ne 2965

This theorem is referenced by:  nelpri  4626  nelprd  4628  eldifpr  4629  0nelop  5480  om00  8559  om00el  8560  oeoe  8584  mulne0b  11854  xmulpnf1  13299  lcmgcd  16664  lcmdvds  16665  domnmuln0  20793  isdomn3  20798  drngmulne0  20843  abvn0b  20916  lvecvsn0  21210  mdetralt  22733  ply1domn  26249  vieta1lem1  26439  vieta1lem2  26440  atandm  27006  atandm3  27008  dchrelbas3  27367  mulsne0bd  28344  eupth2lem3lem7  30525  frgrreg  30685  nmlno0lem  31085  nmlnop0iALT  32287  chirredi  32686  nelpr  32817  minplyirred  34045  subfacp1lem1  35569  filnetlem4  36780  disjecxrn  38950  lcvbr3  39686  cvrnbtwn4  39942  elpadd0  40472  cdleme0moN  40888  cdleme0nex  40953  mulltgt0d  43145  mullt0b2d  43147  sn-mullt0d  43148  fsuppind  43213  lidldomnnring  48889