Theorem neanior 3019

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   ∨ wo 847   = wceq 1540   ≠ wne 2926

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 207  df-an 396  df-or 848  df-ne 2927

This theorem is referenced by:  nelpri  4622  nelprd  4624  eldifpr  4625  0nelop  5459  om00  8542  om00el  8543  oeoe  8566  mulne0b  11826  xmulpnf1  13241  lcmgcd  16584  lcmdvds  16585  domnmuln0  20625  isdomn3  20631  drngmulne0  20678  abvn0b  20752  lvecvsn0  21026  mdetralt  22502  ply1domn  26036  vieta1lem1  26225  vieta1lem2  26226  atandm  26793  atandm3  26795  dchrelbas3  27156  mulsne0bd  28096  eupth2lem3lem7  30170  frgrreg  30330  nmlno0lem  30729  nmlnop0iALT  31931  chirredi  32330  nelpr  32467  minplyirred  33708  subfacp1lem1  35173  filnetlem4  36376  disjecxrn  38382  lcvbr3  39023  cvrnbtwn4  39279  elpadd0  39810  cdleme0moN  40226  cdleme0nex  40291  mulltgt0d  42477  mullt0b2d  42479  sn-mullt0d  42480  fsuppind  42585  lidldomnnring  48228