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  3191  intasym  5320  relcoi1  5473  funres11  5593  cnvresid  5595  elnn  6595  fparlem1  6781  fparlem2  6782  dftpos4  6873  tposf12  6879  tfr2b  6964  tz7.44lem1  6970  xpcomco  7510  sbthlem2  7531  fidomdm  7703  marypha1lem  7793  hartogslem1  7866  brwdom2  7898  inf3lem6  7949  omex  7959  cantnfvalOLD  8016  cnfcom  8043  cnfcomOLD  8051  cnfcom2OLD  8053  cnfcom3lemOLD  8054  cnfcom3OLD  8055  tz9.1c  8060  r1tr  8093  r1ord3g  8096  rankwflemb  8110  r1elwf  8113  r1elss  8123  rankval3b  8143  onssr1  8148  infxpenlem  8290  alephnbtwn  8351  alephordilem1  8353  alephfp  8388  dfac13  8421  pwsdompw  8483  infcdaabs  8485  ackbij1  8517  ackbij2  8522  r1om  8523  cflim2  8542  fin23lem27  8607  fin23lem29  8620  fin23lem30  8621  fin1a2lem6  8684  fin1a2lem7  8685  fin1a2lem13  8691  itunitc1  8699  itunitc  8700  ituniiun  8701  hsmexlem5  8709  axcc2lem  8715  axcc3  8717  zorn2lem6  8780  zorn2lem7  8781  ttukeylem6  8793  axdc  8800  fodom  8801  iunfo  8813  cardval  8820  cardid  8821  pwcfsdom  8857  alephom  8859  fpwwe  8923  canthp1lem2  8930  canthp1  8931  gchaleph2  8949  r1limwun  9013  inaprc  9113  nqerf  9209  recmulnq  9243  dmrecnq  9247  halfnq  9255  genpdm  9281  reclem3pr  9328  axresscn  9425  axpre-sup  9446  1re  9495  0re  9496  00id  9654  addid1  9659  renegcli  9780  zexALT  10775  uzn0  10986  dfle2  11234  xrinfmss  11382  axdc4uzlem  11920  facnn  12169  fac0  12170  hashgval  12222  hashinf  12224  hashresfn  12227  hashrabrsn  12254  hashp1i  12278  hashxplem  12312  brfi1uzind  12336  cshw1  12573  cats1fv  12603  cnrecnv  12771  rexanuz  12950  climdm  13149  lo1eq  13163  rlimeq  13164  sumsn  13334  tanval  13529  rpnnen2lem11  13624  rpnnen  13626  sadadd2lem  13772  sadadd3  13774  sadaddlem  13779  sadasslem  13783  sadeq  13785  3prm  13897  unbenlem  14086  prmreclem6  14099  vdwlem8  14166  vdwnnlem1  14173  0ram  14198  structcnvcnv  14302  prdsval  14511  prdsbas  14513  prdsplusg  14514  prdsmulr  14515  prdsvsca  14516  prdshom  14523  xpsfrn  14625  xpsff1o2  14627  catcoppccl  15094  catcfuccl  15095  catcxpccl  15135  tsrss  15511  gsumpropd2lem  15623  symgid  16024  mvdco  16069  efgmnvl  16331  efgval  16334  efgi0  16337  efgi1  16338  efgredeu  16369  0frgp  16396  lt6abl  16491  gsumval3OLD  16502  gsumval3  16505  gsumzresOLD  16512  gsumzaddOLD  16531  gsum2dlem2  16583  gsum2dOLD  16585  dprdfaddOLD  16638  dprdres  16646  dmdprdsplit2lem  16665  isdrng2  16964  drngmcl  16967  drngid2  16970  psrplusg  17574  coe1sfi  17791  coe1sfiOLD  17792  ply1plusgfvi  17819  cnfldplusf  17967  cnfldsub  17968  cnsubmlem  17985  cnmsubglem  17999  gzrngunitlem  18001  rge0srg  18006  zring0  18017  zrng0  18023  mulgghm2OLD  18052  zzngim  18109  zrhpsgnmhm  18138  re0g  18166  pjfval  18255  pjpm  18257  marep01ma  18597  smadiadetlem1a  18600  smadiadetlem3lem2  18604  smadiadetlem3  18605  smadiadetlem4  18606  smadiadet  18607  indistpsALT  18748  tgrest  18894  leordtval2  18947  lmbr2  18994  cnprest  19024  lmff  19036  kgenidm  19251  tx1cn  19313  tx2cn  19314  hausdiag  19349  tsmsresOLD  19848  elrnust  19930  ustbas  19933  ustuqtop0  19946  utopsnneiplem  19953  neipcfilu  20002  psmetge0  20019  xmetge0  20050  qdensere  20480  cnblcld  20485  cnfldms  20486  cnfldtopn  20492  xrsdsre  20518  xrge0tsms  20542  iccpnfcnv  20647  xrhmeo  20649  cnheiborlem  20657  lmmbr2  20901  lmcau  20954  cmetss  20956  cncms  20998  cnfldcusp  21000  ovolctb  21104  ovoliunnul  21121  ismbl  21140  volf  21143  voliunlem1  21163  ioorf  21185  ioorinv  21188  ioorcl  21189  dyaddisj  21208  dyadmax  21210  dyadmbl  21212  mbfid  21246  ismbfd  21250  mbfimaopnlem  21265  limcresi  21492  dvreslem  21516  dvres2lem  21517  dvcjbr  21555  dvferm1  21589  dvferm2  21591  dvlip2  21599  dv11cn  21605  deg1ldg  21695  deg1leb  21698  plycpn  21887  vieta1lem2  21909  elqaa  21920  aalioulem2  21931  aaliou3lem3  21942  aaliou3lem4  21944  pserulm  22019  psercnlem2  22021  psercnlem1  22022  psercn  22023  abelth  22038  reeff1o  22044  pilem1  22048  efhalfpi  22065  coseq0negpitopi  22097  pige3  22111  tanregt0  22127  efif1olem3  22132  efif1olem4  22133  efifo  22135  eff1olem  22136  logrn  22142  ellogrn  22143  relogf1o  22150  argregt0  22191  argrege0  22192  dvrelog  22214  dvloglem  22225  logf1o2  22227  dvlog  22228  efopnlem1  22233  efopnlem2  22234  logtayl  22237  cxpcn3lem  22317  cxpcn3  22318  resqrcn  22319  asinneg  22413  asinrebnd  22428  atan0  22435  atanbnd  22453  areambl  22484  sqrlim  22498  amgmlem  22515  basellem1  22550  basellem4  22553  sqff1o  22652  dchrplusg  22718  bposlem6  22760  bposlem8  22762  dchrvmasumlem2  22879  mulog2sum  22918  pntibndlem1  22970  pntlemo  22988  qrng0  23002  ostth  23020  constr1trl  23638  vdegp1ai  23756  grporn  23850  issubgoi  23948  gidsn  23986  ginvsn  23987  rngomndo  24059  ip0i  24376  ubthlem1  24422  ubthlem2  24423  axhcompl-zf  24551  normlem7  24669  bcseqi  24673  bcsiALT  24732  hlimf  24791  hlimuni  24792  hhshsslem1  24819  hhsssh  24821  hhsscms  24831  occllem  24857  occl  24858  h1deoi  25103  h1dei  25104  h1de2ctlem  25109  h1de2ci  25110  spansni  25111  spanunsni  25133  pjpythi  25276  nmfn0  25542  nmopadjlem  25644  adjcoi  25655  nmopcoadji  25656  pjoccoi  25733  shatomistici  25916  ceqsexv2d  26033  imadifxp  26089  xppreima  26114  1stpreima  26151  2ndpreima  26152  dmct  26164  xrge0neqmnf  26296  xrge0tsmsd  26397  reofld  26452  rearchi  26454  nn0archi  26455  xrge0slmod  26456  iistmd  26476  xpinpreima  26480  xpinpreima2  26481  tpr2rico  26486  mndpluscn  26500  xrge0pluscn  26514  cnzh  26543  rezh  26544  rrhcn  26570  cnrrext  26583  zrhre  26589  qqhre  26590  sigaex  26696  brsiga  26741  cntnevol  26786  voliune  26788  ddemeas  26795  1stmbfm  26818  2ndmbfm  26819  br2base  26827  dya2icoseg2  26836  dya2iocucvr  26842  eulerpartlemt  26897  eulerpartgbij  26898  eulerpartlemmf  26901  eulerpartlemgvv  26902  eulerpartlemgf  26905  sseqmw  26917  sseqf  26918  sseqp1  26921  fiblem  26924  fibp1  26927  dstrvprob  26997  coinflipspace  27006  coinfliprv  27008  coinflippv  27009  ballotlem1  27012  ballotlem8  27062  lgamucov  27167  iccllyscon  27282  rellyscon  27283  dfrdg2  27752  omsinds  27823  trpredlem1  27834  trpredtr  27837  trpredmintr  27838  wfrlem14  27880  dfrdg4  28124  imagesset  28127  elhf  28355  limsucncmpi  28434  ovoliunnfl  28580  voliunnfl  28582  mbfresfi  28585  dvtanlem  28588  dvtan  28589  itg2addnc  28593  ftc1anclem3  28616  areacirc  28636  filnetlem3  28748  fdc  28788  ismrer1  28884  reheibor  28885  ac6s6f  29132  2rexfrabdioph  29281  3rexfrabdioph  29282  4rexfrabdioph  29283  6rexfrabdioph  29284  7rexfrabdioph  29285  rencldnfi  29307  jm2.27dlem2  29506  wepwso  29542  dfac11  29562  pwssplit4  29589  frlmpwfi  29600  isnumbasgrplem3  29608  mpaaeu  29654  proot1mul  29711  proot1hash  29715  seff  29742  sumsnd  29895  stoweidlem34  29976  stoweidlem37  29979  stirlinglem11  30026  stirlinglem12  30027  hashrabsn01  30379  hashrabsn1  30380  abln0  31142  rngn0  31146  lmodn0  31155  zlmodzxzldeplem3  31162  lvecpsslmod  31167  elimhyps  32935  dedths  32936  tendo0co2  34755  erng1r  34962  dvalveclem  34993  dva0g  34995  dvh0g  35079  taupilem3  35935