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

Theorem neeq1d 2734
Description: Deduction for inequality. (Contributed by NM, 25-Oct-1999.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
Hypothesis
Ref Expression
neeq1d.1
Assertion
Ref Expression
neeq1d

Proof of Theorem neeq1d
StepHypRef Expression
1 neeq1d.1 . . 3
21eqeq1d 2459 . 2
32necon3bid 2715 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  =/=wne 2652
This theorem is referenced by:  neeq12dOLD  2737  neeq1  2738  eqnetrd  2750  prnzg  4150  f12dfv  6179  f13dfv  6180  suppval1  6924  elsuppfn  6926  suppsnop  6932  ressuppss  6938  ressuppssdif  6940  tz7.49  7129  ereldm  7374  pw2f1olem  7641  marypha1lem  7913  wdomtr  8022  inf3lem2  8067  cantnflem1  8129  cantnf  8133  cantnfOLD  8155  cplem2  8329  dfac9  8537  kmlem12  8562  infpssrlem4  8707  fin23lem14  8734  axcc2lem  8837  axcc3  8839  domtriomlem  8843  axdc2lem  8849  ac6c4  8882  zorn2lem6  8902  rpnnen1lem4  11240  rpnnen1lem5  11241  mptnn0fsuppr  12105  hashprg  12460  hashtpg  12523  prodfn0  13703  prodfrec  13704  prodfdiv  13705  ntrivcvgtail  13709  fproddiv  13766  fprodn0  13783  dvdsle  14031  algcvg  14205  algcvga  14208  eucalgcvga  14215  rpdvds  14265  phibndlem  14300  dfphi2  14304  pcaddlem  14407  vdwmc  14496  iscatd2  15078  sgrp2nmndlem5  16047  symgextf1lem  16445  pmtrmvd  16481  frgpup3lem  16795  isirred  17348  isdrngrd  17422  rrgsupp  17939  dsmmelbas  18770  dsmmacl  18772  frlmssuvc2  18826  frlmssuvc2OLD  18828  elcls  19574  clsndisj  19576  elcls3  19584  neindisj2  19624  clslp  19649  cmpfi  19908  cmpfii  19909  dfcon2  19920  consuba  19921  nconsubb  19924  1stcelcls  19962  finlocfin  20021  locfincmp  20027  dissnlocfin  20030  locfindis  20031  ptclsg  20116  dfac14lem  20118  isfbas  20330  trfbas2  20344  isfil  20348  filss  20354  fbunfip  20370  fgval  20371  elfg  20372  isufil2  20409  ufileu  20420  filufint  20421  fmfnfm  20459  flimclslem  20485  fclsopni  20516  fclsnei  20520  fclsbas  20522  fclsrest  20525  fclscmp  20531  ufilcmp  20533  isfcf  20535  fcfnei  20536  fcfneii  20538  ptcmplem2  20553  cnextcn  20567  cnextfres  20568  tsmsfbas  20626  iscusp  20802  cuspcvg  20804  lpbl  21006  prdsxmslem2  21032  restmetu  21090  qdensere  21277  lebnumlem3  21463  isphtpc  21494  iscmet  21723  cmetcvg  21724  equivcmet  21754  cmetcusp1OLD  21791  cmetcusp1  21792  cmetcuspOLD  21793  cmetcusp  21794  rrxmvallem  21831  ovolicc2lem2  21929  ovolicc2lem5  21932  i1fres  22112  lhop1lem  22414  deg1ldg  22492  plyco0  22589  plyeq0lem  22607  coeeq2  22639  coe1termlem  22655  taylfval  22754  cxpeq0  23059  ftalem4  23349  ftalem5  23350  ftalem6  23351  isppw  23388  isnsqf  23409  sqff1o  23456  musum  23467  dchrelbas3  23513  dchrelbasd  23514  dchrelbas4  23518  dchrmulcl  23524  dchrn0  23525  dchrfi  23530  dchrptlem2  23540  dchrpt  23542  lgsne0  23608  lgsdchr  23623  2sqlem11  23650  ishlg  23986  uvtx01vtx  24492  usg2cwwkdifex  24821  frgraregorufr  25053  clwwlkextfrlem1  25076  numclwwlkovh  25101  numclwwlk2lem1  25102  numclwlk2lem2f  25103  numclwlk2lem2f1o  25105  numclwwlk5  25112  nmorepnf  25683  nmoprepnf  26786  nmfnrepnf  26799  disjdsct  27521  locfinreflem  27843  sibfof  28282  signswch  28518  signstfvneq0  28529  derangenlem  28615  subfacp1lem3  28626  subfacp1lem5  28628  subfacp1lem6  28629  subfacp1  28630  iscvm  28704  cvmcov  28708  cvmcov2  28720  eldm3  29191  elima4  29209  nobndlem2  29453  nobndlem4  29455  nobndlem5  29456  nobndlem6  29457  nobndlem8  29459  nobndup  29460  nobnddown  29461  nofulllem5  29466  mblfinlem3  30053  itg2addnclem3  30068  neibastop1  30177  neibastop2lem  30178  neibastop2  30179  neibastop3  30180  neifg  30189  sstotbnd2  30270  cntotbnd  30292  heibor1lem  30305  pellexlem3  30767  inisegn0  30989  mncn0  31088  aaitgo  31111  cvgdvgrat  31194  binomcxplemnotnn0  31261  fproddivf  31588  islptre  31625  islpcn  31645  lptre2pt  31646  0ellimcdiv  31655  stoweidlem28  31810  stoweidlem43  31825  dirkercncflem2  31886  fourierdlem46  31935  fourierdlem79  31968  elaa2lem  32016  elaa2  32017  ovn0ssdmfun  32455  brcic  32582  cicer  32590  nzerooringczr  32880  rmsupp0  32961  scmsuppss  32965  suppmptcfin  32972  linc1  33026  el0ldep  33067  ldepspr  33074  islindeps2  33084  zlmodzxzldeplem4  33104  zlmodzxzldep  33105  ldepsnlinclem1  33106  ldepsnlinclem2  33107  ldepsnlinc  33109  secval  33141  cscval  33142  cotval  33143  2llnm3N  35293  dalem4  35389  cdlemk28-3  36634  mapdh9a  37517
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-cleq 2449  df-ne 2654
  Copyright terms: Public domain W3C validator