Theorem neanior 3053

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

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   ∧ wa 401   ∨ wo 861   = wceq 1570   ≠ wne 2960

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ne 2961

This theorem is used by:  nelpri  4623  nelprd  4625  eldifpr  4626  0nelop  5481  om00  8566  om00el  8567  oeoe  8591  mulne0b  11870  xmulpnf1  13316  lcmgcd  16687  lcmdvds  16688  domnmuln0  20858  isdomn3  20863  drngmulne0  20915  abvn0b  20989  lvecvsn0  21283  mdetralt  22815  ply1domn  26332  vieta1lem1  26522  vieta1lem2  26523  atandm  27092  atandm3  27094  dchrelbas3  27453  mulsne0bd  28430  eupth2lem3lem7  30656  frgrreg  30816  nmlno0lem  31216  nmlnop0iALT  32418  chirredi  32817  nelpr  32948  minplyirred  34165  subfacp1lem1  35708  filnetlem4  36949  disjecxrn  39119  lcvbr3  39855  cvrnbtwn4  40111  elpadd0  40641  cdleme0moN  41057  cdleme0nex  41122  mulltgt0d  43314  mullt0b2d  43316  sn-mullt0d  43317  fsuppind  43380  lidldomnnring  49058