Theorem neanior 3023

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 2931	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		df-ne 2931	. . 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 1541   ≠ wne 2930

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 2931

This theorem is referenced by:  nelpri  4610  nelprd  4612  eldifpr  4613  0nelop  5442  om00  8500  om00el  8501  oeoe  8525  mulne0b  11776  xmulpnf1  13187  lcmgcd  16532  lcmdvds  16533  domnmuln0  20640  isdomn3  20646  drngmulne0  20693  abvn0b  20767  lvecvsn0  21062  mdetralt  22550  ply1domn  26083  vieta1lem1  26272  vieta1lem2  26273  atandm  26840  atandm3  26842  dchrelbas3  27203  mulsne0bd  28155  eupth2lem3lem7  30258  frgrreg  30418  nmlno0lem  30817  nmlnop0iALT  32019  chirredi  32418  nelpr  32555  minplyirred  33817  subfacp1lem1  35322  filnetlem4  36524  disjecxrn  38536  lcvbr3  39222  cvrnbtwn4  39478  elpadd0  40008  cdleme0moN  40424  cdleme0nex  40489  mulltgt0d  42679  mullt0b2d  42681  sn-mullt0d  42682  fsuppind  42775  lidldomnnring  48424