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

Theorem mp2b 10
Description: A double modus ponens inference. (Contributed by Mario Carneiro, 24-Jan-2013.)
Hypotheses
Ref Expression
mp2b.1
mp2b.2
mp2b.3
Assertion
Ref Expression
mp2b

Proof of Theorem mp2b
StepHypRef Expression
1 mp2b.1 . . 3
2 mp2b.2 . . 3
31, 2ax-mp 5 . 2
4 mp2b.3 . 2
53, 4ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4
This theorem is referenced by:  eqvinc  3226  dtru  4643  intasym  5387  relcoi1  5541  funres11  5661  cnvresid  5663  elnn  6710  fparlem1  6900  fparlem2  6901  dftpos4  6993  tposf12  6999  tfr2b  7084  tz7.44lem1  7090  xpcomco  7627  sbthlem2  7648  fidomdm  7822  marypha1lem  7913  hartogslem1  7988  brwdom2  8020  inf3lem6  8071  omex  8081  cantnfvalOLD  8138  cnfcom  8165  cnfcomOLD  8173  cnfcom2OLD  8175  cnfcom3lemOLD  8176  cnfcom3OLD  8177  tz9.1c  8182  r1tr  8215  r1ord3g  8218  rankwflemb  8232  r1elwf  8235  r1elss  8245  rankval3b  8265  onssr1  8270  infxpenlem  8412  alephnbtwn  8473  alephordilem1  8475  alephfp  8510  dfac13  8543  pwsdompw  8605  infcdaabs  8607  ackbij1  8639  ackbij2  8644  r1om  8645  cflim2  8664  fin23lem27  8729  fin23lem29  8742  fin23lem30  8743  fin1a2lem6  8806  fin1a2lem7  8807  fin1a2lem13  8813  itunitc1  8821  itunitc  8822  ituniiun  8823  hsmexlem5  8831  axcc2lem  8837  axcc3  8839  zorn2lem6  8902  zorn2lem7  8903  ttukeylem6  8915  axdc  8922  fodom  8923  iunfo  8935  cardval  8942  cardid  8943  pwcfsdom  8979  alephom  8981  fpwwe  9045  canthp1lem2  9052  canthp1  9053  gchaleph2  9071  r1limwun  9135  inaprc  9235  nqerf  9329  recmulnq  9363  dmrecnq  9367  halfnq  9375  genpdm  9401  reclem3pr  9448  axresscn  9546  axpre-sup  9567  1re  9616  0re  9617  00id  9776  addid1  9781  renegcli  9903  zexALT  10908  uzn0  11125  dfle2  11382  xrinfmss  11530  axdc4uzlem  12092  facnn  12355  fac0  12356  hashgval  12408  hashinf  12410  hashresfn  12413  hashrabrsn  12440  hashrabsn01  12441  hashrabsn1  12442  hashp1i  12468  hashxplem  12491  brfi1uzind  12532  cshw1  12790  cats1fv  12824  cnrecnv  12998  rexanuz  13178  climdm  13377  lo1eq  13391  rlimeq  13392  sumsn  13563  tanval  13863  rpnnen2lem11  13958  rpnnen  13960  sadadd2lem  14109  sadadd3  14111  sadaddlem  14116  sadasslem  14120  sadeq  14122  3prm  14234  unbenlem  14426  prmreclem6  14439  vdwlem8  14506  vdwnnlem1  14513  0ram  14538  structcnvcnv  14643  prdsval  14852  prdsbas  14854  prdsplusg  14855  prdsmulr  14856  prdsvsca  14857  prdshom  14864  xpsfrn  14966  xpsff1o2  14968  catcoppccl  15435  catcfuccl  15436  catcxpccl  15476  tsrss  15853  gsumpropd2lem  15900  symgid  16426  mvdco  16470  efgmnvl  16732  efgval  16735  efgi0  16738  efgi1  16739  efgredeu  16770  0frgp  16797  abln0  16873  lt6abl  16897  gsumval3OLD  16908  gsumval3  16911  gsumzresOLD  16918  gsumzaddOLD  16937  gsum2dlem2  16998  gsum2dOLD  17000  dprdfaddOLD  17067  dprdres  17075  dmdprdsplit2lem  17094  ringn0  17249  isdrng2  17406  drngmcl  17409  drngid2  17412  psrplusg  18034  coe1sfi  18252  coe1sfiOLD  18253  ply1plusgfvi  18283  cnfldplusf  18445  cnfldsub  18446  cnsubmlem  18466  cnmsubglem  18480  gzrngunitlem  18482  rge0srg  18487  zring0  18498  zrng0  18505  mulgghm2OLD  18534  zzngim  18591  zrhpsgnmhm  18620  re0g  18648  pjfval  18737  pjpm  18739  marep01ma  19162  smadiadetlem1a  19165  smadiadetlem3lem2  19169  smadiadetlem3  19170  smadiadetlem4  19171  smadiadet  19172  indistpsALT  19514  tgrest  19660  leordtval2  19713  lmbr2  19760  cnprest  19790  lmff  19802  kgenidm  20048  tx1cn  20110  tx2cn  20111  hausdiag  20146  tsmsresOLD  20645  elrnust  20727  ustbas  20730  ustuqtop0  20743  utopsnneiplem  20750  neipcfilu  20799  psmetge0  20816  xmetge0  20847  qdensere  21277  cnblcld  21282  cnfldms  21283  cnfldtopn  21289  xrsdsre  21315  xrge0tsms  21339  iccpnfcnv  21444  xrhmeo  21446  cnheiborlem  21454  lmmbr2  21698  lmcau  21751  cmetss  21753  cncms  21795  cnfldcusp  21797  ovolctb  21901  ovoliunnul  21918  ismbl  21937  volf  21940  voliunlem1  21960  ioorf  21982  ioorinv  21985  ioorcl  21986  dyaddisj  22005  dyadmax  22007  dyadmbl  22009  mbfid  22043  ismbfd  22047  mbfimaopnlem  22062  limcresi  22289  dvreslem  22313  dvres2lem  22314  dvcjbr  22352  dvferm1  22386  dvferm2  22388  dvlip2  22396  dv11cn  22402  deg1ldg  22492  deg1leb  22495  plycpn  22685  vieta1lem2  22707  elqaa  22718  aalioulem2  22729  aaliou3lem3  22740  aaliou3lem4  22742  pserulm  22817  psercnlem2  22819  psercnlem1  22820  psercn  22821  abelth  22836  reeff1o  22842  pilem1  22846  efhalfpi  22864  coseq0negpitopi  22896  pige3  22910  tanregt0  22926  efif1olem3  22931  efif1olem4  22932  efifo  22934  eff1olem  22935  efsubm  22938  logrn  22946  ellogrn  22947  relogf1o  22954  argregt0  22995  argrege0  22996  dvrelog  23018  dvloglem  23029  logf1o2  23031  dvlog  23032  efopnlem1  23037  efopnlem2  23038  logtayl  23041  cxpcn3lem  23121  cxpcn3  23122  resqrtcn  23123  asinneg  23217  asinrebnd  23232  atan0  23239  atanbnd  23257  areambl  23288  sqrtlim  23302  amgmlem  23319  basellem1  23354  basellem4  23357  sqff1o  23456  dchrplusg  23522  bposlem6  23564  bposlem8  23566  dchrvmasumlem2  23683  mulog2sum  23722  pntibndlem1  23774  pntlemo  23792  qrng0  23806  ostth  23824  lmif  24151  islmib  24153  usgraexmpledg  24403  constr1trl  24590  vdegp1ai  24984  grporn  25214  issubgoi  25312  gidsn  25350  ginvsn  25351  efghgrpOLD  25375  rngomndo  25423  ip0i  25740  ubthlem1  25786  ubthlem2  25787  axhcompl-zf  25915  normlem7  26033  bcseqi  26037  bcsiALT  26096  hlimf  26155  hlimuni  26156  hhshsslem1  26183  hhsssh  26185  hhsscms  26195  occllem  26221  occl  26222  h1deoi  26467  h1dei  26468  h1de2ctlem  26473  h1de2ci  26474  spansni  26475  spanunsni  26497  pjpythi  26640  nmfn0  26906  nmopadjlem  27008  adjcoi  27019  nmopcoadji  27020  pjoccoi  27097  shatomistici  27280  ceqsexv2d  27397  imadifxp  27458  idssxp  27469  xppreima  27487  1stpreima  27524  2ndpreima  27525  dmct  27537  xrge0neqmnf  27679  xrge0tsmsd  27775  reofld  27830  rearchi  27832  nn0archi  27833  xrge0slmod  27834  qtophaus  27839  iistmd  27884  xpinpreima  27888  xpinpreima2  27889  tpr2rico  27894  mndpluscn  27908  xrge0pluscn  27922  cnzh  27951  rezh  27952  qqhucn  27973  rrhcn  27978  cnrrext  27991  zrhre  27997  qqhre  27998  ismntop  28004  sigaex  28109  brsiga  28154  cntnevol  28199  voliune  28201  ddemeas  28208  1stmbfm  28231  2ndmbfm  28232  br2base  28240  dya2icoseg2  28249  dya2iocucvr  28255  eulerpartlemt  28310  eulerpartgbij  28311  eulerpartlemmf  28314  eulerpartlemgvv  28315  eulerpartlemgf  28318  eulerpart  28321  sseqmw  28330  sseqf  28331  sseqp1  28334  fiblem  28337  fibp1  28340  dstrvprob  28410  coinflipspace  28419  coinfliprv  28421  coinflippv  28422  ballotlem1  28425  ballotlem8  28475  lgamucov  28580  iccllyscon  28695  rellyscon  28696  msrid  28905  dfrdg2  29228  omsinds  29299  trpredlem1  29310  trpredtr  29313  trpredmintr  29314  wfrlem14  29356  dfrdg4  29600  imagesset  29603  elhf  29831  limsucncmpi  29910  mblfinlem1  30051  ovoliunnfl  30056  voliunnfl  30058  mbfresfi  30061  dvtanlem  30064  dvtan  30065  itg2addnc  30069  ftc1anclem3  30092  areacirc  30112  filnetlem3  30198  fdc  30238  ismrer1  30334  reheibor  30335  ac6s6f  30581  2rexfrabdioph  30729  3rexfrabdioph  30730  4rexfrabdioph  30731  6rexfrabdioph  30732  7rexfrabdioph  30733  rencldnfi  30755  jm2.27dlem2  30952  wepwso  30988  dfac11  31008  pwssplit4  31035  frlmpwfi  31046  isnumbasgrplem3  31054  mpaaeu  31099  proot1mul  31156  proot1hash  31160  seff  31189  prmunb2  31191  lcmgcdlem  31212  binomcxplemdvbinom  31258  binomcxplemcvg  31259  binomcxplemnotnn0  31261  sumsnd  31401  sumsnf  31570  islptre  31625  stoweidlem34  31816  stoweidlem37  31819  stirlinglem11  31866  stirlinglem12  31867  stirlinglem13  31868  fouriersw  32014  2zrng0  32744  lmodn0  33096  zlmodzxzldeplem3  33103  lvecpsslmod  33108  aacllem  33216  elimhyps  34692  dedths  34693  tendo0co2  36514  erng1r  36721  dvalveclem  36752  dva0g  36754  dvh0g  36838  taupilem3  37694
This theorem was proved from axioms:  ax-mp 5
  Copyright terms: Public domain W3C validator