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

Theorem mp2b 9
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  2896  elnn  4665  intasym  5057  relcoi1  5199  funres11  5286  cnvresid  5288  fvex  5500  fparlem1  6180  fparlem2  6181  dftpos4  6215  tposf12  6221  tfr2b  6408  tz7.44lem1  6414  xpcomco  6948  sbthlem2  6968  fidomdm  7134  marypha1lem  7182  hartogslem1  7253  brwdom2  7283  inf3lem6  7330  omex  7340  cantnfdm  7361  cantnfval  7365  cantnff  7371  cnfcom  7399  cnfcom2  7401  cnfcom3lem  7402  cnfcom3  7403  tz9.1c  7408  r1tr  7444  r1ord3g  7447  rankwflemb  7461  r1elwf  7464  r1elss  7474  rankval3b  7494  onssr1  7499  infxpenlem  7637  alephnbtwn  7694  alephordilem1  7696  alephfp  7731  dfac13  7764  pwsdompw  7826  infcdaabs  7828  ackbij1  7860  ackbij2  7865  r1om  7866  cflim2  7885  fin23lem27  7950  fin23lem29  7963  fin23lem30  7964  fin1a2lem6  8027  fin1a2lem7  8028  fin1a2lem13  8034  itunitc1  8042  itunitc  8043  ituniiun  8044  hsmexlem5  8052  axcc2lem  8058  axcc3  8060  zorn2lem6  8124  zorn2lem7  8125  ttukeylem6  8137  axdc  8144  fodom  8145  iunfo  8157  cardval  8164  cardid  8165  pwcfsdom  8201  alephom  8203  fpwwe  8264  canthp1lem2  8271  canthp1  8272  gchaleph2  8294  r1limwun  8354  inaprc  8454  nqerf  8550  recmulnq  8584  dmrecnq  8588  halfnq  8596  genpdm  8622  reclem3pr  8669  axresscn  8766  axpre-sup  8787  1re  8833  0re  8834  00id  8983  addid1  8988  renegcli  9104  zexALT  10038  uzn0  10239  dfle2  10477  xrinfmss  10624  axdc4uzlem  11040  facnn  11286  fac0  11287  hashgval  11336  hashinf  11338  hashp1i  11365  hashxplem  11381  cats1fv  11505  cnrecnv  11646  rexanuz  11825  climdm  12024  lo1eq  12038  rlimeq  12039  sumsn  12209  tanval  12404  rpnnen2lem11  12499  rpnnen  12501  sadadd2lem  12646  sadadd3  12648  sadaddlem  12653  sadasslem  12657  sadeq  12659  3prm  12771  unbenlem  12951  prmreclem6  12964  vdwlem8  13031  vdwnnlem1  13038  0ram  13063  structcnvcnv  13155  prdsval  13351  prdsbas  13353  prdsplusg  13354  prdsmulr  13355  prdsvsca  13356  prdshom  13362  xpsfrn  13467  xpsff1o2  13469  catcoppccl  13936  catcfuccl  13937  catcxpccl  13977  tsrss  14328  symgid  14777  efgmnvl  15019  efgval  15022  efgi0  15025  efgi1  15026  efgredeu  15057  0frgp  15084  lt6abl  15177  gsumval3  15187  gsumzres  15190  gsumzadd  15200  gsum2d  15219  dprdfadd  15251  dprdres  15259  dmdprdsplit2lem  15276  isdrng2  15518  drngmcl  15521  drngid2  15524  psrplusg  16122  coe1sfi  16289  ply1plusgfvi  16316  cnfldplusf  16397  cnfldsub  16398  cnsubmlem  16415  cnmsubglem  16430  gzrngunitlem  16432  mulgghm2  16455  zzngim  16502  pjfval  16602  pjpm  16604  indistpsALT  16746  tgrest  16886  leordtval2  16938  lmbr2  16985  cnprest  17013  lmff  17025  kgenidm  17238  tx1cn  17299  tx2cn  17300  hausdiag  17335  tsmsres  17822  xmetge0  17905  qdensere  18275  cnblcld  18280  cnfldms  18281  cnfldtopn  18287  xrsdsre  18312  xrge0tsms  18335  iccpnfcnv  18438  xrhmeo  18440  cnheiborlem  18448  lmmbr2  18681  lmcau  18734  cmetss  18736  cncms  18770  ovolctb  18845  ovoliunnul  18862  ismbl  18881  volf  18884  voliunlem1  18903  ioorf  18924  ioorinv  18927  ioorcl  18928  dyaddisj  18947  dyadmax  18949  dyadmbl  18951  mbfid  18987  ismbfd  18991  mbfimaopnlem  19006  limcresi  19231  dvreslem  19255  dvres2lem  19256  dvcjbr  19294  dvferm1  19328  dvferm2  19330  dvlip2  19338  dv11cn  19344  tdeglem4  19442  deg1ldg  19474  deg1leb  19477  plycpn  19665  vieta1lem2  19687  elqaa  19698  aalioulem2  19709  aaliou3lem3  19720  aaliou3lem4  19722  pserulm  19794  psercnlem2  19796  psercnlem1  19797  psercn  19798  abelth  19813  reeff1o  19819  pilem1  19823  efhalfpi  19835  coseq0negpitopi  19867  pige3  19881  efif1olem3  19902  efif1olem4  19903  efifo  19905  eff1olem  19906  logrn  19912  ellogrn  19913  relogf1o  19920  argregt0  19960  argrege0  19961  dvrelog  19980  dvloglem  19991  logf1o2  19993  dvlog  19994  efopnlem1  19999  efopnlem2  20000  logtayl  20003  cxpcn3lem  20083  cxpcn3  20084  resqrcn  20085  asinneg  20178  asinrebnd  20193  atan0  20200  atanbnd  20218  areambl  20249  sqrlim  20263  amgmlem  20280  basellem1  20314  basellem4  20317  sqff1o  20416  dchrplusg  20482  bposlem6  20524  bposlem8  20526  lgseisenlem4  20587  dchrvmasumlem2  20643  dchrisum0flblem1  20653  mulog2sum  20682  pntibndlem1  20734  pntlemo  20752  qrng0  20766  ostth  20784  grporn  20873  issubgoi  20971  gidsn  21009  ginvsn  21010  rngomndo  21082  ip0i  21397  ubthlem1  21443  ubthlem2  21444  axhcompl-zf  21574  normlem7  21691  bcseqi  21695  bcsiALT  21754  hlimf  21813  hlimuni  21814  hhshsslem1  21840  hhsssh  21842  hhsscms  21852  occllem  21878  occl  21879  h1deoi  22124  h1dei  22125  h1de2ctlem  22130  h1de2ci  22131  spansni  22132  spanunsni  22154  pjpythi  22297  nmopadjlem  22665  adjcoi  22676  nmopcoadji  22677  pjoccoi  22754  shatomistici  22937  ballotlem1  23041  iccllyscon  23188  rellyscon  23189  vdegp1ai  23315  dfrdg2  23556  omsinds  23623  trpredlem1  23634  trpredtr  23637  trpredmintr  23638  wfrlem14  23673  dfrdg4  23898  elhf  24214  limsucncmpi  24294  areacirc  24341  scprefat  24481  scprefat2  24482  repfuntw  24571  domrancur1c  24613  bsi  24912  limptlimpr2lem2  24986  dtt1  24999  intrn  25010  bsi2  25050  bsi3  25052  bsi4  25054  addcanri  25077  issrc  25278  tartarmap  25299  prismorcsetlemc  25328  idcatfun  25352  lemindclsbu  25406  pgapspf  25463  pdiveql  25579  filnetlem3  25740  fdc  25866  ismrer1  25973  reheibor  25974  2rexfrabdioph  26288  3rexfrabdioph  26289  4rexfrabdioph  26290  6rexfrabdioph  26291  7rexfrabdioph  26292  rencldnfi  26315  jm2.27dlem2  26514  wepwso  26550  dfac11  26571  pwssplit4  26602  frlmpwfi  26673  isnumbasgrplem3  26681  mpaaeu  26766  mvdco  26799  proot1mul  26926  proot1hash  26930  seff  26949  sumsnd  27108  stoweidlem34  27194  stoweidlem37  27197  tendo0co2  30256  erng1r  30463  dvalveclem  30494  dva0g  30496  dvh0g  30580
This theorem was proved from axioms:  ax-mp 8
  Copyright terms: Public domain W3C validator