Theorem neanior 3033

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

Syntax hints:  ¬ wn 3   ↔ wb 205   ∧ wa 394   ∨ wo 843   = wceq 1539   ≠ wne 2938

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 395  df-or 844  df-ne 2939

This theorem is referenced by:  nelpri  4656  nelprd  4658  eldifpr  4659  0nelop  5495  om00  8577  om00el  8578  oeoe  8601  mulne0b  11859  xmulpnf1  13257  lcmgcd  16548  lcmdvds  16549  drngmulne0  20530  lvecvsn0  20867  domnmuln0  21114  abvn0b  21120  mdetralt  22330  ply1domn  25876  vieta1lem1  26059  vieta1lem2  26060  atandm  26617  atandm3  26619  dchrelbas3  26977  eupth2lem3lem7  29754  frgrreg  29914  nmlno0lem  30313  nmlnop0iALT  31515  chirredi  31914  nelpr  32035  minplyirred  33059  subfacp1lem1  34468  filnetlem4  35569  disjecxrn  37562  lcvbr3  38196  cvrnbtwn4  38452  elpadd0  38983  cdleme0moN  39399  cdleme0nex  39464  fsuppind  41464  isdomn3  42248  lidldomnnring  46916