Theorem neanior 3018

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   ∨ wo 847   = wceq 1540   ≠ wne 2925

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 207  df-an 396  df-or 848  df-ne 2926

This theorem is referenced by:  nelpri  4615  nelprd  4617  eldifpr  4618  0nelop  5451  om00  8516  om00el  8517  oeoe  8540  mulne0b  11795  xmulpnf1  13210  lcmgcd  16553  lcmdvds  16554  domnmuln0  20594  isdomn3  20600  drngmulne0  20647  abvn0b  20721  lvecvsn0  20995  mdetralt  22471  ply1domn  26005  vieta1lem1  26194  vieta1lem2  26195  atandm  26762  atandm3  26764  dchrelbas3  27125  mulsne0bd  28065  eupth2lem3lem7  30136  frgrreg  30296  nmlno0lem  30695  nmlnop0iALT  31897  chirredi  32296  nelpr  32433  minplyirred  33674  subfacp1lem1  35139  filnetlem4  36342  disjecxrn  38348  lcvbr3  38989  cvrnbtwn4  39245  elpadd0  39776  cdleme0moN  40192  cdleme0nex  40257  mulltgt0d  42443  mullt0b2d  42445  sn-mullt0d  42446  fsuppind  42551  lidldomnnring  48197