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

Theorem neneqd 2659
Description: Deduction eliminating inequality definition. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypothesis
Ref Expression
neneqd.1
Assertion
Ref Expression
neneqd

Proof of Theorem neneqd
StepHypRef Expression
1 neneqd.1 . 2
2 df-ne 2654 . 2
31, 2sylib 196 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  =wceq 1395  =/=wne 2652
This theorem is referenced by:  necon3ad  2667  necon2bi  2694  necon2i  2700  necon4i  2701  pm2.21ddne  2771  nelrdva  3309  disjprg  4448  0inp0  4624  onnseq  7034  sniffsupp  7889  ackbij1lem15  8635  ttukeylem7  8916  fpwwe2lem13  9041  canthnumlem  9047  canthp1lem2  9052  recgt0  10411  elnnz  10899  xrnemnf  11357  xrnepnf  11358  fzprval  11769  expnnval  12169  elprchashprn2  12461  sgnp  12923  ruclem12  13974  dvdsle  14031  sqgcd  14196  eucalgf  14212  eucalginv  14213  qredeu  14248  divgcdodd  14260  rpdvds  14265  divnumden  14281  divdenle  14282  oddprm  14339  pythagtriplem4  14343  pythagtriplem8  14347  pythagtriplem9  14348  pythagtriplem19  14357  4sqlem10  14465  ram0  14540  isipodrs  15791  gsumval2  15907  mulgnn  16148  sylow1lem1  16618  gsumval3eu  16907  abvtrivd  17489  00lss  17588  lvecvscan2  17758  fidomndrng  17956  mvridlemOLD  18075  mvrcl  18111  mplmon  18125  mplmonmul  18126  mplcoe3OLD  18129  mplcoe2OLD  18133  evlslem3  18183  coe1tmfv2  18316  cply1coe0  18341  cply1coe0bi  18342  prmirredlem  18523  prmirredlemOLD  18526  uvcff  18822  1marepvsma1  19085  mdetrsca2  19106  mdetrlin2  19109  mdetunilem2  19115  mdetunilem5  19118  mdetunilem6  19119  mdetunilem9  19122  maducoeval2  19142  gsummatr01lem3  19159  gsummatr01lem4  19160  gsummatr01  19161  m2cpm  19242  m2cpminvid2lem  19255  fvmptnn04ifa  19351  fvmptnn04ifb  19352  fvmptnn04ifc  19353  chfacffsupp  19357  chfacfscmul0  19359  chfacfscmulgsum  19361  chfacfpmmul0  19363  chfacfpmmulgsum  19365  conclo  19916  dissnlocfin  20030  ptpjpre2  20081  txindis  20135  snfil  20365  alexsublem  20544  tsmsfbas  20626  stdbdxmet  21018  dscmet  21093  xrsxmet  21314  iccpnfcnv  21444  cphsubrglem  21624  minveclem3b  21843  minveclem4a  21845  ovolicc1  21927  dvexp2  22357  lhop2  22416  deg1sublt  22511  ig1pval3  22575  dvply1  22680  plydiveu  22694  quotcan  22705  aaliou3lem9  22746  taylthlem2  22769  pserdvlem2  22823  abelthlem9  22835  logtayllem  23040  logtayl  23041  cxpef  23046  angrtmuld  23140  isosctrlem2  23153  isosctrlem3  23154  chordthmlem  23163  leibpilem2  23272  leibpi  23273  rlimcnp2  23296  efrlim  23299  vma1  23440  muinv  23469  lgsval2lem  23581  lgsval4  23591  lgsdir  23605  lgseisenlem4  23627  lgsquadlem1  23629  lgsquad2  23635  m1lgs  23637  2sqlem8a  23646  2sqlem8  23647  padicabv  23815  ostth1  23818  ostth3  23823  tgbtwnne  23881  tgbtwndiff  23897  tgcolg  23941  tgbtwnconn1lem3  23961  legso  23985  tglineeltr  24011  tglineintmo  24022  tglineneq  24024  coltr2  24028  colline  24030  miriso  24050  mirhl  24059  mirbtwnhl  24060  symquadlem  24066  krippenlem  24067  midexlem  24069  ragncol  24086  footex  24095  colperp  24103  colperpexlem3  24106  mideulem2  24108  opphllem  24109  midex  24111  opptgdim2  24117  lmieu  24150  axlowdimlem15  24259  axcontlem2  24268  axcontlem7  24273  isusgra0  24347  usgraop  24350  usgra1v  24390  cyclnspth  24631  clwwlkn0  24774  rusgra0edg  24955  eupath2lem1  24977  eupath2lem2  24978  eupath2lem3  24979  gxpval  25261  strlem6  27175  hstrlem6  27183  atssma  27297  chirredlem1  27309  znsqcld  27561  xaddeq0  27573  xlt2addrd  27578  gcdnncl  27607  divnumden2  27609  2sqcoprm  27635  2sqmod  27636  submomnd  27700  ornglmullt  27797  orngrmullt  27798  ofldchr  27804  suborng  27805  xrge0iifcnv  27915  xrge0iifcv  27916  xrge0iif1  27920  qqhval2lem  27962  qqhf  27967  qqhre  27998  logccne0OLD  28011  logccne0  28012  ballotlemirc  28470  sgnmul  28481  sgn0bi  28486  signswlid  28516  fz0n  29110  dfrdg2  29228  nobndup  29460  nobnddown  29461  dfrdg4  29600  broutsideof2  29772  outsidele  29782  rankeq1o  29828  limsucncmpi  29910  ivthALT  30153  fdc  30238  heibor1lem  30305  heiborlem4  30310  heiborlem6  30312  jm2.26lem3  30943  kelac1  31009  phisum  31159  lcmgcdlem  31212  refsum2cnlem1  31412  neneq  31429  oddfl  31459  xrlttri5d  31465  icoiccdif  31564  fmul01lt1lem1  31578  fprodn0f  31594  climrec  31609  limcperiod  31634  reclimc  31659  cncfiooicclem1  31696  cncfioobdlem  31699  dvmptdiv  31714  fperdvper  31715  dvdivbd  31720  ditgeqiooicc  31759  itgsincmulx  31773  itgioocnicc  31776  iblcncfioo  31777  stoweidlem35  31817  stoweidlem39  31821  stirlinglem5  31860  stirlinglem8  31863  dirkerper  31878  dirkercncflem2  31886  dirkercncflem4  31888  fourierdlem31  31920  fourierdlem34  31923  fourierdlem41  31930  fourierdlem42  31931  fourierdlem44  31933  fourierdlem48  31937  fourierdlem49  31938  fourierdlem53  31942  fourierdlem56  31945  fourierdlem58  31947  fourierdlem60  31949  fourierdlem61  31950  fourierdlem62  31951  fourierdlem65  31954  fourierdlem66  31955  fourierdlem73  31962  fourierdlem76  31965  fourierdlem79  31968  fourierdlem81  31970  fourierdlem82  31971  fourierdlem93  31982  fourierdlem103  31992  fourierdlem104  31993  sqwvfoura  32011  fourierswlem  32013  elaa2lem  32016  elaa2  32017  etransclem4  32021  etransclem24  32041  etransclem31  32048  etransclem32  32049  etransclem35  32052  sineq0ALT  33737  bnj1523  34127  2atm  35251  lhpocnle  35740  lhp2at0nle  35759  trlval3  35912  cdleme18c  36018  cdlemg17b  36388  cdlemg17i  36395  dia2dimlem2  36792  dia2dimlem3  36793  dihord6apre  36983  dihatlat  37061  dochshpsat  37181  lcfrlem9  37277  mapdhval2  37453  hdmap1val2  37528  hdmap14lem4a  37601  hdmap14lem6  37603
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