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  |-  ph
mp2b.2  |-  ( ph  ->  ps )
mp2b.3  |-  ( ps 
->  ch )
Assertion
Ref Expression
mp2b  |-  ch

Proof of Theorem mp2b
StepHypRef Expression
1 mp2b.1 . . 3  |-  ph
2 mp2b.2 . . 3  |-  ( ph  ->  ps )
31, 2ax-mp 8 . 2  |-  ps
4 mp2b.3 . 2  |-  ( ps 
->  ch )
53, 4ax-mp 8 1  |-  ch
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  eqvinc  3027  elnn  4818  intasym  5212  relcoi1  5361  funres11  5484  cnvresid  5486  fparlem1  6409  fparlem2  6410  dftpos4  6461  tposf12  6467  tfr2b  6620  tz7.44lem1  6626  xpcomco  7161  sbthlem2  7181  fidomdm  7351  marypha1lem  7400  hartogslem1  7471  brwdom2  7501  inf3lem6  7548  omex  7558  cantnfdm  7579  cantnfval  7583  cantnff  7589  cnfcom  7617  cnfcom2  7619  cnfcom3lem  7620  cnfcom3  7621  tz9.1c  7626  r1tr  7662  r1ord3g  7665  rankwflemb  7679  r1elwf  7682  r1elss  7692  rankval3b  7712  onssr1  7717  infxpenlem  7855  alephnbtwn  7912  alephordilem1  7914  alephfp  7949  dfac13  7982  pwsdompw  8044  infcdaabs  8046  ackbij1  8078  ackbij2  8083  r1om  8084  cflim2  8103  fin23lem27  8168  fin23lem29  8181  fin23lem30  8182  fin1a2lem6  8245  fin1a2lem7  8246  fin1a2lem13  8252  itunitc1  8260  itunitc  8261  ituniiun  8262  hsmexlem5  8270  axcc2lem  8276  axcc3  8278  zorn2lem6  8341  zorn2lem7  8342  ttukeylem6  8354  axdc  8361  fodom  8362  iunfo  8374  cardval  8381  cardid  8382  pwcfsdom  8418  alephom  8420  fpwwe  8481  canthp1lem2  8488  canthp1  8489  gchaleph2  8511  r1limwun  8571  inaprc  8671  nqerf  8767  recmulnq  8801  dmrecnq  8805  halfnq  8813  genpdm  8839  reclem3pr  8886  axresscn  8983  axpre-sup  9004  1re  9050  0re  9051  00id  9201  addid1  9206  renegcli  9322  zexALT  10260  uzn0  10461  dfle2  10700  xrinfmss  10848  axdc4uzlem  11280  facnn  11527  fac0  11528  hashgval  11580  hashinf  11582  hashrabrsn  11607  hashp1i  11631  hashxplem  11655  brfi1uzind  11674  cats1fv  11782  cnrecnv  11929  rexanuz  12108  climdm  12307  lo1eq  12321  rlimeq  12322  sumsn  12493  tanval  12688  rpnnen2lem11  12783  rpnnen  12785  sadadd2lem  12930  sadadd3  12932  sadaddlem  12937  sadasslem  12941  sadeq  12943  3prm  13055  unbenlem  13235  prmreclem6  13248  vdwlem8  13315  vdwnnlem1  13322  0ram  13347  structcnvcnv  13439  prdsval  13637  prdsbas  13639  prdsplusg  13640  prdsmulr  13641  prdsvsca  13642  prdshom  13648  xpsfrn  13753  xpsff1o2  13755  catcoppccl  14222  catcfuccl  14223  catcxpccl  14263  tsrss  14614  symgid  15063  efgmnvl  15305  efgval  15308  efgi0  15311  efgi1  15312  efgredeu  15343  0frgp  15370  lt6abl  15463  gsumval3  15473  gsumzres  15476  gsumzadd  15486  gsum2d  15505  dprdfadd  15537  dprdres  15545  dmdprdsplit2lem  15562  isdrng2  15804  drngmcl  15807  drngid2  15810  psrplusg  16404  coe1sfi  16569  ply1plusgfvi  16595  cnfldplusf  16687  cnfldsub  16688  cnsubmlem  16705  cnmsubglem  16720  gzrngunitlem  16722  mulgghm2  16745  zzngim  16792  pjfval  16892  pjpm  16894  indistpsALT  17036  tgrest  17181  leordtval2  17234  lmbr2  17281  cnprest  17311  lmff  17323  kgenidm  17536  tx1cn  17598  tx2cn  17599  hausdiag  17634  tsmsres  18130  elrnust  18211  ustbas  18214  ustuqtop0  18227  utopsnneiplem  18234  neipcfilu  18283  psmetge0  18300  xmetge0  18331  qdensere  18761  cnblcld  18766  cnfldms  18767  cnfldtopn  18773  xrsdsre  18798  xrge0tsms  18822  iccpnfcnv  18926  xrhmeo  18928  cnheiborlem  18936  lmmbr2  19169  lmcau  19222  cmetss  19224  cncms  19266  cnfldcusp  19268  ovolctb  19343  ovoliunnul  19360  ismbl  19379  volf  19382  voliunlem1  19401  ioorf  19422  ioorinv  19425  ioorcl  19426  dyaddisj  19445  dyadmax  19447  dyadmbl  19449  mbfid  19485  ismbfd  19489  mbfimaopnlem  19504  limcresi  19729  dvreslem  19753  dvres2lem  19754  dvcjbr  19792  dvferm1  19826  dvferm2  19828  dvlip2  19836  dv11cn  19842  tdeglem4  19940  deg1ldg  19972  deg1leb  19975  plycpn  20163  vieta1lem2  20185  elqaa  20196  aalioulem2  20207  aaliou3lem3  20218  aaliou3lem4  20220  pserulm  20295  psercnlem2  20297  psercnlem1  20298  psercn  20299  abelth  20314  reeff1o  20320  pilem1  20324  efhalfpi  20336  coseq0negpitopi  20368  pige3  20382  tanregt0  20398  efif1olem3  20403  efif1olem4  20404  efifo  20406  eff1olem  20407  logrn  20413  ellogrn  20414  relogf1o  20421  argregt0  20462  argrege0  20463  dvrelog  20485  dvloglem  20496  logf1o2  20498  dvlog  20499  efopnlem1  20504  efopnlem2  20505  logtayl  20508  cxpcn3lem  20588  cxpcn3  20589  resqrcn  20590  asinneg  20683  asinrebnd  20698  atan0  20705  atanbnd  20723  areambl  20754  sqrlim  20768  amgmlem  20785  basellem1  20820  basellem4  20823  sqff1o  20922  dchrplusg  20988  bposlem6  21030  bposlem8  21032  lgseisenlem4  21093  dchrvmasumlem2  21149  dchrisum0flblem1  21159  mulog2sum  21188  pntibndlem1  21240  pntlemo  21258  qrng0  21272  ostth  21290  constr1trl  21545  vdegp1ai  21663  grporn  21757  issubgoi  21855  gidsn  21893  ginvsn  21894  rngomndo  21966  ip0i  22283  ubthlem1  22329  ubthlem2  22330  axhcompl-zf  22458  normlem7  22575  bcseqi  22579  bcsiALT  22638  hlimf  22697  hlimuni  22698  hhshsslem1  22724  hhsssh  22726  hhsscms  22736  occllem  22762  occl  22763  h1deoi  23008  h1dei  23009  h1de2ctlem  23014  h1de2ci  23015  spansni  23016  spanunsni  23038  pjpythi  23181  nmfn0  23447  nmopadjlem  23549  adjcoi  23560  nmopcoadji  23561  pjoccoi  23638  shatomistici  23821  ceqsexv2d  23942  imadifxp  23995  xppreima  24016  1stpreima  24052  2ndpreima  24053  dmct  24063  hashresfn  24113  xrge0neqmnf  24169  gsumpropd2lem  24177  xrge0tsmsd  24180  zzs0  24224  re0g  24230  iistmd  24257  xpinpreima  24261  xpinpreima2  24262  tpr2rico  24267  mndpluscn  24269  xrge0pluscn  24283  cnzh  24311  rezh  24312  zrhre  24342  qqhre  24343  rrhre  24344  sigaex  24449  brsiga  24494  cntnevol  24539  voliune  24542  1stmbfm  24567  2ndmbfm  24568  br2base  24576  dya2iocucvr  24591  dstrvprob  24686  coinflipspace  24695  coinfliprv  24697  coinflippv  24698  ballotlem1  24701  ballotlem8  24751  lgamucov  24779  iccllyscon  24894  rellyscon  24895  dfrdg2  25370  omsinds  25437  trpredlem1  25448  trpredtr  25451  trpredmintr  25452  wfrlem14  25487  dfrdg4  25707  elhf  26023  limsucncmpi  26103  ovoliunnfl  26151  voliunnfl  26153  mbfresfi  26156  itg2addnc  26162  areacirc  26191  filnetlem3  26303  fdc  26343  ismrer1  26441  reheibor  26442  2rexfrabdioph  26750  3rexfrabdioph  26751  4rexfrabdioph  26752  6rexfrabdioph  26753  7rexfrabdioph  26754  rencldnfi  26776  jm2.27dlem2  26975  wepwso  27011  dfac11  27032  pwssplit4  27063  frlmpwfi  27134  isnumbasgrplem3  27142  mpaaeu  27227  mvdco  27260  proot1mul  27387  proot1hash  27391  seff  27410  sumsnd  27568  stoweidlem34  27654  stoweidlem37  27657  stirlinglem11  27704  stirlinglem12  27705  tendo0co2  31274  erng1r  31481  dvalveclem  31512  dva0g  31514  dvh0g  31598
This theorem was proved from axioms:  ax-mp 8
  Copyright terms: Public domain W3C validator