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

Step	Hyp	Ref	Expression
1		mp2b.1	. . 3 |- ph
2		mp2b.2	. . 3 |- ( ph -> ps )
3	1, 2	ax-mp 5	. 2 |- ps
4		mp2b.3	. 2 |- ( ps -> ch )
5	3, 4	ax-mp 5	1 |- ch

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-mp 5

This theorem is referenced by:  minimp-sylsimp  1561  ceqsexv2d  3243  dtru  4857  intasym  5511  relcoi2  5663  funres11  5966  cnvresid  5968  idssxp  6009  elnn  7075  omsinds  7084  fparlem1  7277  fparlem2  7278  dftpos4  7371  tposf12  7377  wfrlem14  7428  tfr2b  7492  tz7.44lem1  7501  xpcomco  8050  sbthlem2  8071  fidomdm  8243  hartogslem1  8447  brwdom2  8478  inf3lem6  8530  omex  8540  cnfcom  8597  tz9.1c  8606  r1tr  8639  r1ord3g  8642  rankwflemb  8656  r1elwf  8659  r1elss  8669  rankval3b  8689  onssr1  8694  infxpenlem  8836  alephnbtwn  8894  alephordilem1  8896  alephfp  8931  dfac13  8964  pwsdompw  9026  infcdaabs  9028  ackbij1  9060  ackbij2  9065  r1om  9066  cflim2  9085  fin23lem27  9150  fin23lem29  9163  fin23lem30  9164  fin1a2lem6  9227  fin1a2lem7  9228  fin1a2lem13  9234  itunitc1  9242  itunitc  9243  ituniiun  9244  hsmexlem5  9252  axcc2lem  9258  axcc3  9260  zorn2lem6  9323  zorn2lem7  9324  ttukeylem6  9336  axdc  9343  fodom  9344  dmct  9346  iunfo  9361  cardval  9368  cardid  9369  pwcfsdom  9405  alephom  9407  canthp1lem2  9475  canthp1  9476  gchaleph2  9494  r1limwun  9558  inaprc  9658  nqerf  9752  recmulnq  9786  dmrecnq  9790  halfnq  9798  genpdm  9824  reclem3pr  9871  axresscn  9969  axpre-sup  9990  1re  10039  0re  10040  00id  10211  addid1  10216  renegcli  10342  zexALT  11396  uzn0  11703  dfle2  11980  xrinfmss  12140  xrge0neqmnf  12276  axdc4uzlem  12782  facnn  13062  fac0  13063  hashgval  13120  hashinf  13122  hashresfn  13128  hashrabrsn  13161  hashrabsn01  13162  hashrabsn1  13163  hashp1i  13191  hashxplem  13220  fi1uzind  13279  fi1uzindOLD  13285  cshw1  13568  cats1fv  13604  trclubgi  13737  trclubgiOLD  13738  cnrecnv  13905  rexanuz  14085  climdm  14285  lo1eq  14299  rlimeq  14300  sumsnf  14473  sumsn  14475  tanval  14858  rpnnen2lem11  14953  rpnnen  14956  sadadd2lem  15181  sadadd3  15183  sadaddlem  15188  sadasslem  15192  sadeq  15194  lcmgcdlem  15319  3prm  15406  unbenlem  15612  prmreclem6  15625  vdwlem8  15692  vdwnnlem1  15699  0ram  15724  structcnvcnv  15871  prdsval  16115  prdsbas  16117  prdsplusg  16118  prdsmulr  16119  prdsvsca  16120  prdshom  16127  xpsfrn  16229  xpsff1o2  16231  catcoppccl  16758  catcfuccl  16759  catcxpccl  16847  tsrss  17223  gsumpropd2lem  17273  symgid  17821  mvdco  17865  efgmnvl  18127  efgval  18130  efgi0  18133  efgi1  18134  efgredeu  18165  0frgp  18192  abln0  18270  lt6abl  18296  gsumval3  18308  gsum2dlem2  18370  dprdres  18427  dmdprdsplit2lem  18444  ringn0  18603  isdrng2  18757  drngmcl  18760  drngid2  18763  psrplusg  19381  coe1sfi  19583  ply1plusgfvi  19612  cnfldplusf  19773  cnfldsub  19774  cnsubmlem  19794  cnmsubglem  19809  gzrngunitlem  19811  rge0srg  19817  zring0  19828  zzngim  19901  zrhpsgnmhm  19930  re0g  19958  pjfval  20050  pjpm  20052  marep01ma  20466  smadiadetlem1a  20469  smadiadetlem3lem2  20473  smadiadetlem3  20474  smadiadetlem4  20475  smadiadet  20476  indistpsALT  20817  tgrest  20963  leordtval2  21016  lmbr2  21063  cnprest  21093  lmff  21105  kgenidm  21350  tx1cn  21412  tx2cn  21413  hausdiag  21448  elrnust  22028  ustbas  22031  psmetge0  22117  xmetge0  22149  qdensere  22573  cnblcld  22578  cnfldms  22579  cnfldtopn  22585  xrsdsre  22613  xrge0tsms  22637  iccpnfcnv  22743  xrhmeo  22745  cnheiborlem  22753  cnlmod  22940  lmmbr2  23057  lmcau  23111  cmetss  23113  cncms  23151  cnfldcusp  23153  ovolctb  23258  ovoliunnul  23275  ismbl  23294  volf  23297  voliunlem1  23318  ioorf  23341  ioorinv  23344  ioorcl  23345  dyaddisj  23364  dyadmax  23366  dyadmbl  23368  mbfid  23403  ismbfd  23407  mbfimaopnlem  23422  limcresi  23649  dvreslem  23673  dvres2lem  23674  dvcjbr  23712  dvferm1  23748  dvferm2  23750  dvlip2  23758  dv11cn  23764  deg1ldg  23852  deg1leb  23855  plycpn  24044  vieta1lem2  24066  elqaa  24077  aalioulem2  24088  aaliou3lem3  24099  aaliou3lem4  24101  pserulm  24176  psercnlem2  24178  psercnlem1  24179  psercn  24180  abelth  24195  reeff1o  24201  pilem1  24205  efhalfpi  24223  coseq0negpitopi  24255  pige3  24269  tanregt0  24285  efif1olem3  24290  efif1olem4  24291  efifo  24293  eff1olem  24294  efsubm  24297  logrn  24305  ellogrn  24306  relogf1o  24313  argregt0  24356  argrege0  24357  dvrelog  24383  dvloglem  24394  logf1o2  24396  dvlog  24397  efopnlem1  24402  efopnlem2  24403  logtayl  24406  cxpcn3lem  24488  cxpcn3  24489  resqrtcn  24490  asinneg  24613  asinrebnd  24628  atan0  24635  atanbnd  24653  areambl  24685  sqrtlim  24699  amgmlem  24716  lgamucov  24764  basellem1  24807  basellem4  24810  sqff1o  24908  dchrplusg  24972  bposlem6  25014  bposlem8  25016  dchrvmasumlem2  25187  mulog2sum  25226  pntibndlem1  25278  pntlemo  25296  qrng0  25310  ostth  25328  lmif  25677  islmib  25679  structiedg0val  25911  snstriedgval  25930  vtxvalsnop  25933  iedgvalsnop  25934  umgredgnlp  26042  usgrexmplef  26151  usgrexmpledg  26154  vtxdlfgrval  26381  upgr2pthnlp  26628  konigsberglem5  27118  ex-mod  27306  pliguhgr  27338  grporn  27375  ip0i  27680  ubthlem1  27726  ubthlem2  27727  axhcompl-zf  27855  normlem7  27973  bcseqi  27977  bcsiALT  28036  hlimf  28094  hlimuni  28095  hhssabloilem  28118  hhshsslem1  28124  hhsssh  28126  hhsscms  28136  occllem  28162  occl  28163  h1deoi  28408  h1dei  28409  h1de2ctlem  28414  h1de2ci  28415  spansni  28416  spanunsni  28438  pjpythi  28581  nmfn0  28846  nmopadjlem  28948  adjcoi  28959  nmopcoadji  28960  pjoccoi  29037  shatomistici  29220  imadifxp  29414  xppreima  29449  1stpreima  29484  2ndpreima  29485  gsummpt2d  29781  xrge0tsmsd  29785  reofld  29840  rearchi  29842  nn0archi  29843  xrge0slmod  29844  qtophaus  29903  iistmd  29948  xpinpreima  29952  xpinpreima2  29953  tpr2rico  29958  mndpluscn  29972  xrge0pluscn  29986  cnzh  30014  rezh  30015  qqhucn  30036  rrhcn  30041  cnrrext  30054  zrhre  30063  qqhre  30064  ismntop  30070  sigaex  30172  brsiga  30246  cntnevol  30291  voliune  30292  ddemeas  30299  1stmbfm  30322  2ndmbfm  30323  br2base  30331  dya2icoseg2  30340  dya2iocucvr  30346  carsgclctunlem2  30381  carsgclctunlem3  30382  sitgaddlemb  30410  eulerpartlemt  30433  eulerpartgbij  30434  eulerpartlemmf  30437  eulerpartlemgvv  30438  eulerpartlemgf  30441  eulerpart  30444  sseqmw  30453  sseqf  30454  sseqp1  30457  fiblem  30460  fibp1  30463  dstrvprob  30533  coinflipspace  30542  coinfliprv  30544  coinflippv  30545  ballotlem1  30548  ballotlem8  30598  circlemethhgt  30721  iccllysconn  31232  rellysconn  31233  msrid  31442  dfrdg2  31701  trpredlem1  31727  trpredtr  31730  trpredmintr  31731  noextendseq  31820  dfrdg4  32058  imagesset  32060  elhf  32281  filnetlem3  32375  limsucncmpi  32444  taupilem3  33165  icoreresf  33200  icoreelrnab  33202  relowlssretop  33211  poimirlem3  33412  poimirlem9  33418  poimirlem15  33424  poimirlem16  33425  poimirlem17  33426  poimirlem19  33428  poimirlem27  33436  poimirlem28  33437  poimirlem31  33440  poimirlem32  33441  mblfinlem1  33446  ovoliunnfl  33451  voliunnfl  33453  mbfresfi  33456  dvtan  33460  itg2addnc  33464  ftc1anclem3  33487  areacirc  33505  fdc  33541  ismrer1  33637  reheibor  33638  rngomndo  33734  gidsn  33751  ac6s6f  33981  opabf  34131  dedths  34248  tendo0co2  36076  erng1r  36283  dvalveclem  36314  dva0g  36316  dvh0g  36400  2rexfrabdioph  37360  3rexfrabdioph  37361  4rexfrabdioph  37362  6rexfrabdioph  37363  7rexfrabdioph  37364  rencldnfi  37385  jm2.27dlem2  37577  wepwso  37613  dfac11  37632  pwssplit4  37659  frlmpwfi  37668  isnumbasgrplem3  37675  mpaaeu  37720  proot1mul  37777  proot1hash  37778  cnvcnvintabd  37906  rtrclex  37924  cnvrcl0  37932  dfrtrcl5  37936  frege92  38249  seff  38508  prmunb2  38510  binomcxplemdvbinom  38552  binomcxplemcvg  38553  binomcxplemnotnn0  38555  sumsnd  39185  islptre  39851  stoweidlem34  40251  stoweidlem37  40254  stirlinglem11  40301  stirlinglem12  40302  stirlinglem13  40303  fouriersw  40448  fmtnoinf  41448  gbowge7  41651  nnsum3primes4  41676  2zrng0  41938  lmodn0  42284  zlmodzxzldeplem3  42291  lvecpsslmod  42296  0dig2pr01  42404  aacllem  42547  amgmwlem  42548