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:  eqvinc  3081  intasym  5208  relcoi1  5361  funres11  5481  cnvresid  5483  elnn  6481  fparlem1  6667  fparlem2  6668  dftpos4  6759  tposf12  6765  tfr2b  6847  tz7.44lem1  6853  xpcomco  7393  sbthlem2  7414  fidomdm  7585  marypha1lem  7675  hartogslem1  7748  brwdom2  7780  inf3lem6  7831  omex  7841  cantnfvalOLD  7898  cnfcom  7925  cnfcomOLD  7933  cnfcom2OLD  7935  cnfcom3lemOLD  7936  cnfcom3OLD  7937  tz9.1c  7942  r1tr  7975  r1ord3g  7978  rankwflemb  7992  r1elwf  7995  r1elss  8005  rankval3b  8025  onssr1  8030  infxpenlem  8172  alephnbtwn  8233  alephordilem1  8235  alephfp  8270  dfac13  8303  pwsdompw  8365  infcdaabs  8367  ackbij1  8399  ackbij2  8404  r1om  8405  cflim2  8424  fin23lem27  8489  fin23lem29  8502  fin23lem30  8503  fin1a2lem6  8566  fin1a2lem7  8567  fin1a2lem13  8573  itunitc1  8581  itunitc  8582  ituniiun  8583  hsmexlem5  8591  axcc2lem  8597  axcc3  8599  zorn2lem6  8662  zorn2lem7  8663  ttukeylem6  8675  axdc  8682  fodom  8683  iunfo  8695  cardval  8702  cardid  8703  pwcfsdom  8739  alephom  8741  fpwwe  8805  canthp1lem2  8812  canthp1  8813  gchaleph2  8831  r1limwun  8895  inaprc  8995  nqerf  9091  recmulnq  9125  dmrecnq  9129  halfnq  9137  genpdm  9163  reclem3pr  9210  axresscn  9307  axpre-sup  9328  1re  9377  0re  9378  00id  9536  addid1  9541  renegcli  9662  zexALT  10657  uzn0  10868  dfle2  11116  xrinfmss  11264  axdc4uzlem  11796  facnn  12045  fac0  12046  hashgval  12098  hashinf  12100  hashresfn  12103  hashrabrsn  12129  hashp1i  12153  hashxplem  12187  brfi1uzind  12211  cshw1  12448  cats1fv  12478  cnrecnv  12646  rexanuz  12825  climdm  13024  lo1eq  13038  rlimeq  13039  sumsn  13209  tanval  13404  rpnnen2lem11  13499  rpnnen  13501  sadadd2lem  13647  sadadd3  13649  sadaddlem  13654  sadasslem  13658  sadeq  13660  3prm  13772  unbenlem  13961  prmreclem6  13974  vdwlem8  14041  vdwnnlem1  14048  0ram  14073  structcnvcnv  14177  prdsval  14385  prdsbas  14387  prdsplusg  14388  prdsmulr  14389  prdsvsca  14390  prdshom  14397  xpsfrn  14499  xpsff1o2  14501  catcoppccl  14968  catcfuccl  14969  catcxpccl  15009  tsrss  15385  gsumpropd2lem  15496  symgid  15897  mvdco  15942  efgmnvl  16202  efgval  16205  efgi0  16208  efgi1  16209  efgredeu  16240  0frgp  16267  lt6abl  16362  gsumval3OLD  16373  gsumval3  16376  gsumzresOLD  16383  gsumzaddOLD  16402  gsum2dlem2  16450  gsum2dOLD  16452  dprdfaddOLD  16505  dprdres  16513  dmdprdsplit2lem  16532  isdrng2  16820  drngmcl  16823  drngid2  16826  psrplusg  17429  coe1sfi  17643  coe1sfiOLD  17644  ply1plusgfvi  17672  cnfldplusf  17818  cnfldsub  17819  cnsubmlem  17836  cnmsubglem  17850  gzrngunitlem  17852  rge0srg  17857  zring0  17868  zrng0  17874  mulgghm2OLD  17903  zzngim  17960  zrhpsgnmhm  17989  re0g  18017  pjfval  18106  pjpm  18108  marep01ma  18441  smadiadetlem1a  18444  smadiadetlem3lem2  18448  smadiadetlem3  18449  smadiadetlem4  18450  smadiadet  18451  indistpsALT  18592  tgrest  18738  leordtval2  18791  lmbr2  18838  cnprest  18868  lmff  18880  kgenidm  19095  tx1cn  19157  tx2cn  19158  hausdiag  19193  tsmsresOLD  19692  elrnust  19774  ustbas  19777  ustuqtop0  19790  utopsnneiplem  19797  neipcfilu  19846  psmetge0  19863  xmetge0  19894  qdensere  20324  cnblcld  20329  cnfldms  20330  cnfldtopn  20336  xrsdsre  20362  xrge0tsms  20386  iccpnfcnv  20491  xrhmeo  20493  cnheiborlem  20501  lmmbr2  20745  lmcau  20798  cmetss  20800  cncms  20842  cnfldcusp  20844  ovolctb  20948  ovoliunnul  20965  ismbl  20984  volf  20987  voliunlem1  21006  ioorf  21028  ioorinv  21031  ioorcl  21032  dyaddisj  21051  dyadmax  21053  dyadmbl  21055  mbfid  21089  ismbfd  21093  mbfimaopnlem  21108  limcresi  21335  dvreslem  21359  dvres2lem  21360  dvcjbr  21398  dvferm1  21432  dvferm2  21434  dvlip2  21442  dv11cn  21448  deg1ldg  21538  deg1leb  21541  plycpn  21730  vieta1lem2  21752  elqaa  21763  aalioulem2  21774  aaliou3lem3  21785  aaliou3lem4  21787  pserulm  21862  psercnlem2  21864  psercnlem1  21865  psercn  21866  abelth  21881  reeff1o  21887  pilem1  21891  efhalfpi  21908  coseq0negpitopi  21940  pige3  21954  tanregt0  21970  efif1olem3  21975  efif1olem4  21976  efifo  21978  eff1olem  21979  logrn  21985  ellogrn  21986  relogf1o  21993  argregt0  22034  argrege0  22035  dvrelog  22057  dvloglem  22068  logf1o2  22070  dvlog  22071  efopnlem1  22076  efopnlem2  22077  logtayl  22080  cxpcn3lem  22160  cxpcn3  22161  resqrcn  22162  asinneg  22256  asinrebnd  22271  atan0  22278  atanbnd  22296  areambl  22327  sqrlim  22341  amgmlem  22358  basellem1  22393  basellem4  22396  sqff1o  22495  dchrplusg  22561  bposlem6  22603  bposlem8  22605  dchrvmasumlem2  22722  mulog2sum  22761  pntibndlem1  22813  pntlemo  22831  qrng0  22845  ostth  22863  constr1trl  23438  vdegp1ai  23556  grporn  23650  issubgoi  23748  gidsn  23786  ginvsn  23787  rngomndo  23859  ip0i  24176  ubthlem1  24222  ubthlem2  24223  axhcompl-zf  24351  normlem7  24469  bcseqi  24473  bcsiALT  24532  hlimf  24591  hlimuni  24592  hhshsslem1  24619  hhsssh  24621  hhsscms  24631  occllem  24657  occl  24658  h1deoi  24903  h1dei  24904  h1de2ctlem  24909  h1de2ci  24910  spansni  24911  spanunsni  24933  pjpythi  25076  nmfn0  25342  nmopadjlem  25444  adjcoi  25455  nmopcoadji  25456  pjoccoi  25533  shatomistici  25716  ceqsexv2d  25833  imadifxp  25890  xppreima  25915  1stpreima  25952  2ndpreima  25953  dmct  25965  xrge0neqmnf  26103  xrge0tsmsd  26204  reofld  26260  rearchi  26262  nn0archi  26263  xrge0slmod  26264  iistmd  26284  xpinpreima  26288  xpinpreima2  26289  tpr2rico  26294  mndpluscn  26308  xrge0pluscn  26322  cnzh  26351  rezh  26352  rrhcn  26378  cnrrext  26391  zrhre  26397  qqhre  26398  sigaex  26504  brsiga  26549  cntnevol  26594  voliune  26597  ddemeas  26604  1stmbfm  26627  2ndmbfm  26628  br2base  26636  dya2icoseg2  26645  dya2iocucvr  26651  eulerpartlemt  26706  eulerpartgbij  26707  eulerpartlemmf  26710  eulerpartlemgvv  26711  eulerpartlemgf  26714  sseqmw  26726  sseqf  26727  sseqp1  26730  fiblem  26733  fibp1  26736  dstrvprob  26806  coinflipspace  26815  coinfliprv  26817  coinflippv  26818  ballotlem1  26821  ballotlem8  26871  lgamucov  26976  iccllyscon  27091  rellyscon  27092  dfrdg2  27560  omsinds  27631  trpredlem1  27642  trpredtr  27645  trpredmintr  27646  wfrlem14  27688  dfrdg4  27932  imagesset  27935  elhf  28163  limsucncmpi  28243  ovoliunnfl  28386  voliunnfl  28388  mbfresfi  28391  dvtanlem  28394  dvtan  28395  itg2addnc  28399  ftc1anclem3  28422  areacirc  28442  filnetlem3  28554  fdc  28594  ismrer1  28690  reheibor  28691  ac6s6f  28938  2rexfrabdioph  29087  3rexfrabdioph  29088  4rexfrabdioph  29089  6rexfrabdioph  29090  7rexfrabdioph  29091  rencldnfi  29113  jm2.27dlem2  29312  wepwso  29348  dfac11  29368  pwssplit4  29395  frlmpwfi  29406  isnumbasgrplem3  29414  mpaaeu  29460  proot1mul  29517  proot1hash  29521  seff  29548  sumsnd  29701  stoweidlem34  29782  stoweidlem37  29785  stirlinglem11  29832  stirlinglem12  29833  hashrabsn01  30185  hashrabsn1  30186  abln0  30913  rngn0  30917  lmodn0  30926  zlmodzxzldeplem3  30933  lvecpsslmod  30938  elimhyps  32452  dedths  32453  tendo0co2  34272  erng1r  34479  dvalveclem  34510  dva0g  34512  dvh0g  34596  taupilem3  35452