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  4619  nelprd  4621  eldifpr  4622  0nelop  5456  om00  8539  om00el  8540  oeoe  8563  mulne0b  11819  xmulpnf1  13234  lcmgcd  16577  lcmdvds  16578  domnmuln0  20618  isdomn3  20624  drngmulne0  20671  abvn0b  20745  lvecvsn0  21019  mdetralt  22495  ply1domn  26029  vieta1lem1  26218  vieta1lem2  26219  atandm  26786  atandm3  26788  dchrelbas3  27149  mulsne0bd  28089  eupth2lem3lem7  30163  frgrreg  30323  nmlno0lem  30722  nmlnop0iALT  31924  chirredi  32323  nelpr  32460  minplyirred  33701  subfacp1lem1  35166  filnetlem4  36369  disjecxrn  38375  lcvbr3  39016  cvrnbtwn4  39272  elpadd0  39803  cdleme0moN  40219  cdleme0nex  40284  mulltgt0d  42470  mullt0b2d  42472  sn-mullt0d  42473  fsuppind  42578  lidldomnnring  48224