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  3175  dtru  4584  intasym  5202  relcoi1OLD  5352  funres11  5636  cnvresid  5638  elnn  6692  omsinds  6701  fparlem1  6883  fparlem2  6884  dftpos4  6976  tposf12  6982  wfrlem14  7033  tfr2b  7098  tz7.44lem1  7107  xpcomco  7644  sbthlem2  7665  fidomdm  7835  marypha1lem  7926  hartogslem1  8000  brwdom2  8032  inf3lem6  8082  omex  8092  cantnfvalOLD  8148  cnfcom  8175  cnfcomOLD  8183  cnfcom2OLD  8185  cnfcom3lemOLD  8186  cnfcom3OLD  8187  tz9.1c  8192  r1tr  8225  r1ord3g  8228  rankwflemb  8242  r1elwf  8245  r1elss  8255  rankval3b  8275  onssr1  8280  infxpenlem  8422  alephnbtwn  8483  alephordilem1  8485  alephfp  8520  dfac13  8553  pwsdompw  8615  infcdaabs  8617  ackbij1  8649  ackbij2  8654  r1om  8655  cflim2  8674  fin23lem27  8739  fin23lem29  8752  fin23lem30  8753  fin1a2lem6  8816  fin1a2lem7  8817  fin1a2lem13  8823  itunitc1  8831  itunitc  8832  ituniiun  8833  hsmexlem5  8841  axcc2lem  8847  axcc3  8849  zorn2lem6  8912  zorn2lem7  8913  ttukeylem6  8925  axdc  8932  fodom  8933  iunfo  8945  cardval  8952  cardid  8953  pwcfsdom  8989  alephom  8991  fpwwe  9053  canthp1lem2  9060  canthp1  9061  gchaleph2  9079  r1limwun  9143  inaprc  9243  nqerf  9337  recmulnq  9371  dmrecnq  9375  halfnq  9383  genpdm  9409  reclem3pr  9456  axresscn  9554  axpre-sup  9575  1re  9624  0re  9625  00id  9788  addid1  9793  renegcli  9915  zexALT  10923  uzn0  11141  dfle2  11405  xrinfmss  11553  axdc4uzlem  12131  facnn  12397  fac0  12398  hashgval  12453  hashinf  12455  hashresfn  12458  hashrabrsn  12486  hashrabsn01  12487  hashrabsn1  12488  hashp1i  12515  hashxplem  12538  brfi1uzind  12579  cshw1  12844  cats1fv  12878  trclubgi  12978  cnrecnv  13145  rexanuz  13325  climdm  13524  lo1eq  13538  rlimeq  13539  sumsn  13710  tanval  14070  rpnnen2lem11  14165  rpnnen  14167  sadadd2lem  14316  sadadd3  14318  sadaddlem  14323  sadasslem  14327  sadeq  14329  3prm  14441  unbenlem  14633  prmreclem6  14646  vdwlem8  14713  vdwnnlem1  14720  0ram  14745  structcnvcnv  14850  prdsval  15067  prdsbas  15069  prdsplusg  15070  prdsmulr  15071  prdsvsca  15072  prdshom  15079  xpsfrn  15181  xpsff1o2  15183  catcoppccl  15709  catcfuccl  15710  catcxpccl  15798  tsrss  16175  gsumpropd2lem  16222  symgid  16748  mvdco  16792  efgmnvl  17054  efgval  17057  efgi0  17060  efgi1  17061  efgredeu  17092  0frgp  17119  abln0  17195  lt6abl  17219  gsumval3OLD  17230  gsumval3  17233  gsumzresOLD  17240  gsumzaddOLD  17259  gsum2dlem2  17317  gsum2dOLD  17319  dprdfaddOLD  17385  dprdres  17393  dmdprdsplit2lem  17412  ringn0  17567  isdrng2  17724  drngmcl  17727  drngid2  17730  psrplusg  18352  coe1sfi  18570  coe1sfiOLD  18571  ply1plusgfvi  18601  cnfldplusf  18763  cnfldsub  18764  cnsubmlem  18784  cnmsubglem  18798  gzrngunitlem  18800  rge0srg  18805  zring0  18816  zzngim  18887  zrhpsgnmhm  18916  re0g  18944  pjfval  19033  pjpm  19035  marep01ma  19452  smadiadetlem1a  19455  smadiadetlem3lem2  19459  smadiadetlem3  19460  smadiadetlem4  19461  smadiadet  19462  indistpsALT  19804  tgrest  19951  leordtval2  20004  lmbr2  20051  cnprest  20081  lmff  20093  kgenidm  20338  tx1cn  20400  tx2cn  20401  hausdiag  20436  tsmsresOLD  20935  elrnust  21017  ustbas  21020  ustuqtop0  21033  utopsnneiplem  21040  neipcfilu  21089  psmetge0  21106  xmetge0  21137  qdensere  21567  cnblcld  21572  cnfldms  21573  cnfldtopn  21579  xrsdsre  21605  xrge0tsms  21629  iccpnfcnv  21734  xrhmeo  21736  cnheiborlem  21744  lmmbr2  21988  lmcau  22041  cmetss  22043  cncms  22085  cnfldcusp  22087  ovolctb  22191  ovoliunnul  22208  ismbl  22227  volf  22230  voliunlem1  22250  ioorf  22272  ioorinv  22275  ioorcl  22276  dyaddisj  22295  dyadmax  22297  dyadmbl  22299  mbfid  22333  ismbfd  22337  mbfimaopnlem  22352  limcresi  22579  dvreslem  22603  dvres2lem  22604  dvcjbr  22642  dvferm1  22676  dvferm2  22678  dvlip2  22686  dv11cn  22692  deg1ldg  22782  deg1leb  22785  plycpn  22975  vieta1lem2  22997  elqaa  23008  aalioulem2  23019  aaliou3lem3  23030  aaliou3lem4  23032  pserulm  23107  psercnlem2  23109  psercnlem1  23110  psercn  23111  abelth  23126  reeff1o  23132  pilem1  23136  efhalfpi  23154  coseq0negpitopi  23186  pige3  23200  tanregt0  23216  efif1olem3  23221  efif1olem4  23222  efifo  23224  eff1olem  23225  efsubm  23228  logrn  23236  ellogrn  23237  relogf1o  23244  argregt0  23287  argrege0  23288  dvrelog  23310  dvloglem  23321  logf1o2  23323  dvlog  23324  efopnlem1  23329  efopnlem2  23330  logtayl  23333  cxpcn3lem  23415  cxpcn3  23416  resqrtcn  23417  asinneg  23540  asinrebnd  23555  atan0  23562  atanbnd  23580  areambl  23612  sqrtlim  23626  amgmlem  23643  lgamucov  23691  basellem1  23733  basellem4  23736  sqff1o  23835  dchrplusg  23901  bposlem6  23943  bposlem8  23945  dchrvmasumlem2  24062  mulog2sum  24101  pntibndlem1  24153  pntlemo  24171  qrng0  24185  ostth  24203  lmif  24534  islmib  24536  usgraexmpledg  24807  constr1trl  24994  vdegp1ai  25388  grporn  25614  issubgoi  25712  gidsn  25750  ginvsn  25751  efghgrpOLD  25775  rngomndo  25823  ip0i  26140  ubthlem1  26186  ubthlem2  26187  axhcompl-zf  26315  normlem7  26433  bcseqi  26437  bcsiALT  26496  hlimf  26555  hlimuni  26556  hhshsslem1  26583  hhsssh  26585  hhsscms  26595  occllem  26621  occl  26622  h1deoi  26867  h1dei  26868  h1de2ctlem  26873  h1de2ci  26874  spansni  26875  spanunsni  26897  pjpythi  27040  nmfn0  27305  nmopadjlem  27407  adjcoi  27418  nmopcoadji  27419  pjoccoi  27496  shatomistici  27679  ceqsexv2d  27798  imadifxp  27880  idssxp  27896  xppreima  27916  1stpreima  27955  2ndpreima  27956  dmct  27969  xrge0neqmnf  28117  gsummpt2d  28209  xrge0tsmsd  28214  reofld  28269  rearchi  28271  nn0archi  28272  xrge0slmod  28273  qtophaus  28278  iistmd  28323  xpinpreima  28327  xpinpreima2  28328  tpr2rico  28333  mndpluscn  28347  xrge0pluscn  28361  cnzh  28389  rezh  28390  qqhucn  28411  rrhcn  28416  cnrrext  28429  zrhre  28435  qqhre  28436  ismntop  28442  sigaex  28543  brsiga  28617  cntnevol  28662  voliune  28664  ddemeas  28671  1stmbfm  28694  2ndmbfm  28695  br2base  28703  dya2icoseg2  28712  dya2iocucvr  28718  carsgclctunlem2  28753  carsgclctunlem3  28754  eulerpartlemt  28802  eulerpartgbij  28803  eulerpartlemmf  28806  eulerpartlemgvv  28807  eulerpartlemgf  28810  eulerpart  28813  sseqmw  28822  sseqf  28823  sseqp1  28826  fiblem  28829  fibp1  28832  dstrvprob  28902  coinflipspace  28911  coinfliprv  28913  coinflippv  28914  ballotlem1  28917  ballotlem8  28967  iccllyscon  29534  rellyscon  29535  msrid  29744  dfrdg2  30002  trpredlem1  30028  trpredtr  30031  trpredmintr  30032  dfrdg4  30276  imagesset  30278  elhf  30499  filnetlem3  30595  limsucncmpi  30664  taupilem3  31232  icoreresf  31256  icoreelrnab  31258  relowlssretop  31266  mblfinlem1  31403  ovoliunnfl  31408  voliunnfl  31410  mbfresfi  31413  dvtanlemOLD  31417  dvtan  31418  itg2addnc  31422  ftc1anclem3  31445  areacirc  31463  fdc  31500  ismrer1  31596  reheibor  31597  ac6s6f  31843  elimhyps  31965  dedths  31966  tendo0co2  33787  erng1r  33994  dvalveclem  34025  dva0g  34027  dvh0g  34111  2rexfrabdioph  35071  3rexfrabdioph  35072  4rexfrabdioph  35073  6rexfrabdioph  35074  7rexfrabdioph  35075  rencldnfi  35096  jm2.27dlem2  35294  wepwso  35330  dfac11  35350  pwssplit4  35377  frlmpwfi  35390  isnumbasgrplem3  35398  mpaaeu  35443  proot1mul  35500  proot1hash  35504  frege92  35916  seff  36017  prmunb2  36019  lcmgcdlem  36040  binomcxplemdvbinom  36086  binomcxplemcvg  36087  binomcxplemnotnn0  36089  sumsnd  36761  sumsnf  36919  islptre  36974  stoweidlem34  37165  stoweidlem37  37168  stirlinglem11  37215  stirlinglem12  37216  stirlinglem13  37217  fouriersw  37363  gboge7  37798  nnsum3primes4  37817  2zrng0  38236  lmodn0  38588  zlmodzxzldeplem3  38595  lvecpsslmod  38600  0dig2pr01  38722  aacllem  38841