Theorem neanior 3037

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

Syntax hints:  ¬ wn 3   ↔ wb 205   ∧ wa 396   ∨ wo 844   = wceq 1539   ≠ wne 2943

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 397  df-or 845  df-ne 2944

This theorem is referenced by:  nelpri  4590  nelprd  4592  eldifpr  4593  0nelop  5410  om00  8406  om00el  8407  oeoe  8430  mulne0b  11616  xmulpnf1  13008  lcmgcd  16312  lcmdvds  16313  drngmulne0  20013  lvecvsn0  20371  domnmuln0  20569  abvn0b  20573  mdetralt  21757  ply1domn  25288  vieta1lem1  25470  vieta1lem2  25471  atandm  26026  atandm3  26028  dchrelbas3  26386  eupth2lem3lem7  28598  frgrreg  28758  nmlno0lem  29155  nmlnop0iALT  30357  chirredi  30756  nelpr  30879  subfacp1lem1  33141  filnetlem4  34570  lcvbr3  37037  cvrnbtwn4  37293  elpadd0  37823  cdleme0moN  38239  cdleme0nex  38304  fsuppind  40279  isdomn3  41029  lidldomnnring  45488