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

Theorem pm2.61ne 2772
Description: Deduction eliminating an inequality in an antecedent. (Contributed by NM, 24-May-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
Hypotheses
Ref Expression
pm2.61ne.1
pm2.61ne.2
pm2.61ne.3
Assertion
Ref Expression
pm2.61ne

Proof of Theorem pm2.61ne
StepHypRef Expression
1 pm2.61ne.3 . . 3
2 pm2.61ne.1 . . 3
31, 2syl5ibr 221 . 2
4 pm2.61ne.2 . . 3
54expcom 435 . 2
63, 5pm2.61ine 2770 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  =/=wne 2652
This theorem is referenced by:  pwdom  7689  cantnfle  8111  cantnflem1  8129  cantnf  8133  cantnfleOLD  8141  cantnflem1OLD  8152  cantnfOLD  8155  cdalepw  8597  infmap2  8619  zornn0g  8906  ttukeylem6  8915  msqge0  10099  xrsupsslem  11527  xrinfmsslem  11528  fzoss1  11852  swrdcl  12646  abs1m  13168  fsumcvg3  13551  bezoutlem4  14179  gcdmultiplez  14189  dvdssq  14198  pcdvdsb  14392  pcgcd1  14400  pc2dvds  14402  pcaddlem  14407  qexpz  14420  4sqlem19  14481  prmlem1a  14592  gsumwsubmcl  16006  gsumccat  16009  gsumwmhm  16013  zringlpir  18512  zlpir  18517  mretopd  19593  ufildom1  20427  alexsublem  20544  nmolb2d  21225  nmoi  21235  nmoix  21236  ipcau2  21677  mdegcl  22469  ply1divex  22537  ig1pcl  22576  dgrmulc  22668  mulcxplem  23065  vmacl  23392  efvmacl  23394  vmalelog  23480  padicabv  23815  nmlnoubi  25711  nmblolbii  25714  blocnilem  25719  blocni  25720  ubthlem1  25786  nmbdoplbi  26943  cnlnadjlem7  26992  branmfn  27024  pjbdlni  27068  shatomistici  27280  segcon2  29755  cntzsdrg  31151  lcmid  31215  lssats  34737  ps-1  35201  3atlem5  35211  lplnnle2at  35265  2llnm3N  35293  lvolnle3at  35306  4atex2  35801  cdlemd5  35927  cdleme21k  36064  cdlemg33b  36433  mapdrvallem2  37372  mapdhcl  37454  hdmapval3N  37568  hdmap10  37570  hdmaprnlem17N  37593  hdmap14lem2a  37597  hdmaplkr  37643  hgmapvv  37656
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-an 371  df-ne 2654
  Copyright terms: Public domain W3C validator