Theorem neanior 2886

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

Syntax hints:  ¬ wn 3   ↔ wb 196   ∨ wo 383   ∧ wa 384   = wceq 1483   ≠ wne 2794

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-or 385  df-an 386  df-ne 2795

This theorem is referenced by:  nelpri  4201  nelprd  4203  eldifpr  4204  0nelop  4960  om00  7655  om00el  7656  oeoe  7679  mulne0b  10668  xmulpnf1  12104  lcmgcd  15320  lcmdvds  15321  drngmulne0  18769  lvecvsn0  19109  domnmuln0  19298  abvn0b  19302  mdetralt  20414  ply1domn  23883  vieta1lem1  24065  vieta1lem2  24066  atandm  24603  atandm3  24605  dchrelbas3  24963  eupth2lem3lem7  27094  frgrreg  27252  nmlno0lem  27648  nmlnop0iALT  28854  chirredi  29253  subfacp1lem1  31161  filnetlem4  32376  lcvbr3  34310  cvrnbtwn4  34566  elpadd0  35095  cdleme0moN  35512  cdleme0nex  35577  isdomn3  37782  lidldomnnring  41930