Theorem neanior 3079

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

Syntax hints:  ¬ wn 3   ↔ wb 209   ∧ wa 399   ∨ wo 844   = wceq 1538   ≠ wne 2987

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 400  df-or 845  df-ne 2988

This theorem is referenced by:  nelpri  4554  nelprd  4556  eldifpr  4557  0nelop  5351  om00  8184  om00el  8185  oeoe  8208  mulne0b  11270  xmulpnf1  12655  lcmgcd  15941  lcmdvds  15942  drngmulne0  19517  lvecvsn0  19874  domnmuln0  20064  abvn0b  20068  mdetralt  21213  ply1domn  24724  vieta1lem1  24906  vieta1lem2  24907  atandm  25462  atandm3  25464  dchrelbas3  25822  eupth2lem3lem7  28019  frgrreg  28179  nmlno0lem  28576  nmlnop0iALT  29778  chirredi  30177  nelpr  30303  subfacp1lem1  32539  filnetlem4  33842  lcvbr3  36319  cvrnbtwn4  36575  elpadd0  37105  cdleme0moN  37521  cdleme0nex  37586  fsuppind  39456  isdomn3  40148  lidldomnnring  44554