MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  neanior Structured version   Visualization version   GIF version

Theorem neanior 3106
Description: A De Morgan's law for inequality. (Contributed by NM, 18-May-2007.)
Assertion
Ref Expression
neanior ((𝐴𝐵𝐶𝐷) ↔ ¬ (𝐴 = 𝐵𝐶 = 𝐷))

Proof of Theorem neanior
StepHypRef Expression
1 df-ne 3014 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 df-ne 3014 . . 3 (𝐶𝐷 ↔ ¬ 𝐶 = 𝐷)
31, 2anbi12i 626 . 2 ((𝐴𝐵𝐶𝐷) ↔ (¬ 𝐴 = 𝐵 ∧ ¬ 𝐶 = 𝐷))
4 pm4.56 982 . 2 ((¬ 𝐴 = 𝐵 ∧ ¬ 𝐶 = 𝐷) ↔ ¬ (𝐴 = 𝐵𝐶 = 𝐷))
53, 4bitri 276 1 ((𝐴𝐵𝐶𝐷) ↔ ¬ (𝐴 = 𝐵𝐶 = 𝐷))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 207  wa 396  wo 841   = wceq 1528  wne 3013
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 208  df-an 397  df-or 842  df-ne 3014
This theorem is referenced by:  nelpri  4584  nelprd  4586  eldifpr  4587  0nelop  5377  om00  8190  om00el  8191  oeoe  8214  mulne0b  11269  xmulpnf1  12655  lcmgcd  15939  lcmdvds  15940  drngmulne0  19453  lvecvsn0  19810  domnmuln0  19999  abvn0b  20003  mdetralt  21145  ply1domn  24644  vieta1lem1  24826  vieta1lem2  24827  atandm  25381  atandm3  25383  dchrelbas3  25741  eupth2lem3lem7  27940  frgrreg  28100  nmlno0lem  28497  nmlnop0iALT  29699  chirredi  30098  nelpr  30218  subfacp1lem1  32323  filnetlem4  33626  lcvbr3  36039  cvrnbtwn4  36295  elpadd0  36825  cdleme0moN  37241  cdleme0nex  37306  isdomn3  39682  lidldomnnring  44129
  Copyright terms: Public domain W3C validator