MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  necon3abid Unicode version

Theorem necon3abid 2703
Description: Deduction from equality to inequality. (Contributed by NM, 21-Mar-2007.)
Hypothesis
Ref Expression
necon3abid.1
Assertion
Ref Expression
necon3abid

Proof of Theorem necon3abid
StepHypRef Expression
1 df-ne 2654 . 2
2 necon3abid.1 . . 3
32notbid 294 . 2
41, 3syl5bb 257 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 184  =wceq 1395  =/=wne 2652
This theorem is referenced by:  necon3bbid  2704  necon2abid  2711  foconst  5811  fndmdif  5991  suppsnop  6932  om00el  7244  oeoa  7265  cardsdom2  8390  mulne0b  10215  crne0  10554  expneg  12174  hashsdom  12449  gcdn0gt0  14160  pltval3  15597  mulgnegnn  16152  drngmulne0  17418  lvecvsn0  17755  domnmuln0  17947  mvrf1  18081  connsub  19922  pthaus  20139  xkohaus  20154  bndth  21458  lebnumlem1  21461  dvcobr  22349  dvcnvlem  22377  mdegle0  22477  coemulhi  22651  vieta1lem1  22706  vieta1lem2  22707  aalioulem2  22729  cosne0  22917  atandm3  23209  wilthlem2  23343  issqf  23410  mumullem2  23454  dchrptlem3  23541  lgseisenlem3  23626  brbtwn2  24208  colinearalg  24213  vdn0frgrav2  25023  vdgn0frgrav2  25024  vdn1frgrav2  25025  vdgn1frgrav2  25026  nmlno0lem  25708  nmlnop0iALT  26914  atcvat2i  27306  divnumden2  27609  rencldnfilem  30754  qirropth  30844  binomcxplemfrat  31256  binomcxplemradcnv  31257  bnj1542  33915  bnj1253  34073  llnexchb2  35593  cdlemb3  36332
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 185  df-ne 2654
  Copyright terms: Public domain W3C validator