Theorem neanior 3035

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 612	. 2 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷) ↔ (¬ 𝐴 = 𝐵 ∧ ¬ 𝐶 = 𝐷))
4		pm4.56 973	. 2 ⊢ ((¬ 𝐴 = 𝐵 ∧ ¬ 𝐶 = 𝐷) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷))
5	3, 4	bitri 264	1 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷))

Syntax hints:  ¬ wn 3   ↔ wb 196   ∧ wa 382   ∨ wo 836   = wceq 1631   ≠ 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 197  df-an 383  df-or 837  df-ne 2944

This theorem is referenced by:  nelpri  4341  nelprd  4343  eldifpr  4344  0nelop  5088  om00  7813  om00el  7814  oeoe  7837  mulne0b  10874  xmulpnf1  12309  lcmgcd  15528  lcmdvds  15529  drngmulne0  18979  lvecvsn0  19322  domnmuln0  19513  abvn0b  19517  mdetralt  20632  ply1domn  24103  vieta1lem1  24285  vieta1lem2  24286  atandm  24824  atandm3  24826  dchrelbas3  25184  eupth2lem3lem7  27414  frgrreg  27593  nmlno0lem  27988  nmlnop0iALT  29194  chirredi  29593  subfacp1lem1  31499  filnetlem4  32713  lcvbr3  34830  cvrnbtwn4  35086  elpadd0  35616  cdleme0moN  36033  cdleme0nex  36098  isdomn3  38306  lidldomnnring  42453