Theorem neanior 3025

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 2933	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		df-ne 2933	. . 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 2932

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 2933

This theorem is referenced by:  nelpri  4612  nelprd  4614  eldifpr  4615  0nelop  5444  om00  8502  om00el  8503  oeoe  8527  mulne0b  11778  xmulpnf1  13189  lcmgcd  16534  lcmdvds  16535  domnmuln0  20642  isdomn3  20648  drngmulne0  20695  abvn0b  20769  lvecvsn0  21064  mdetralt  22552  ply1domn  26085  vieta1lem1  26274  vieta1lem2  26275  atandm  26842  atandm3  26844  dchrelbas3  27205  mulsne0bd  28182  eupth2lem3lem7  30309  frgrreg  30469  nmlno0lem  30868  nmlnop0iALT  32070  chirredi  32469  nelpr  32606  minplyirred  33868  subfacp1lem1  35373  filnetlem4  36575  disjecxrn  38597  lcvbr3  39283  cvrnbtwn4  39539  elpadd0  40069  cdleme0moN  40485  cdleme0nex  40550  mulltgt0d  42737  mullt0b2d  42739  sn-mullt0d  42740  fsuppind  42833  lidldomnnring  48482