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  3077  intasym  5203  relcoi1  5356  funres11  5476  cnvresid  5478  elnn  6477  fparlem1  6663  fparlem2  6664  dftpos4  6755  tposf12  6761  tfr2b  6843  tz7.44lem1  6849  xpcomco  7391  sbthlem2  7412  fidomdm  7583  marypha1lem  7673  hartogslem1  7746  brwdom2  7778  inf3lem6  7829  omex  7839  cantnfvalOLD  7896  cnfcom  7923  cnfcomOLD  7931  cnfcom2OLD  7933  cnfcom3lemOLD  7934  cnfcom3OLD  7935  tz9.1c  7940  r1tr  7973  r1ord3g  7976  rankwflemb  7990  r1elwf  7993  r1elss  8003  rankval3b  8023  onssr1  8028  infxpenlem  8170  alephnbtwn  8231  alephordilem1  8233  alephfp  8268  dfac13  8301  pwsdompw  8363  infcdaabs  8365  ackbij1  8397  ackbij2  8402  r1om  8403  cflim2  8422  fin23lem27  8487  fin23lem29  8500  fin23lem30  8501  fin1a2lem6  8564  fin1a2lem7  8565  fin1a2lem13  8571  itunitc1  8579  itunitc  8580  ituniiun  8581  hsmexlem5  8589  axcc2lem  8595  axcc3  8597  zorn2lem6  8660  zorn2lem7  8661  ttukeylem6  8673  axdc  8680  fodom  8681  iunfo  8693  cardval  8700  cardid  8701  pwcfsdom  8737  alephom  8739  fpwwe  8803  canthp1lem2  8810  canthp1  8811  gchaleph2  8829  r1limwun  8893  inaprc  8993  nqerf  9089  recmulnq  9123  dmrecnq  9127  halfnq  9135  genpdm  9161  reclem3pr  9208  axresscn  9305  axpre-sup  9326  1re  9375  0re  9376  00id  9534  addid1  9539  renegcli  9660  zexALT  10655  uzn0  10866  dfle2  11114  xrinfmss  11262  axdc4uzlem  11790  facnn  12039  fac0  12040  hashgval  12092  hashinf  12094  hashresfn  12097  hashrabrsn  12123  hashp1i  12147  hashxplem  12181  brfi1uzind  12205  cshw1  12442  cats1fv  12472  cnrecnv  12640  rexanuz  12819  climdm  13018  lo1eq  13032  rlimeq  13033  sumsn  13203  tanval  13397  rpnnen2lem11  13492  rpnnen  13494  sadadd2lem  13640  sadadd3  13642  sadaddlem  13647  sadasslem  13651  sadeq  13653  3prm  13765  unbenlem  13954  prmreclem6  13967  vdwlem8  14034  vdwnnlem1  14041  0ram  14066  structcnvcnv  14170  prdsval  14378  prdsbas  14380  prdsplusg  14381  prdsmulr  14382  prdsvsca  14383  prdshom  14390  xpsfrn  14492  xpsff1o2  14494  catcoppccl  14961  catcfuccl  14962  catcxpccl  15002  tsrss  15378  symgid  15888  mvdco  15933  efgmnvl  16193  efgval  16196  efgi0  16199  efgi1  16200  efgredeu  16231  0frgp  16258  lt6abl  16353  gsumval3OLD  16364  gsumval3  16367  gsumzresOLD  16374  gsumzaddOLD  16393  gsum2dlem2  16438  gsum2dOLD  16440  dprdfaddOLD  16493  dprdres  16501  dmdprdsplit2lem  16520  isdrng2  16768  drngmcl  16771  drngid2  16774  psrplusg  17388  coe1sfi  17569  coe1sfiOLD  17570  ply1plusgfvi  17597  cnfldplusf  17689  cnfldsub  17690  cnsubmlem  17707  cnmsubglem  17721  gzrngunitlem  17723  zring0  17737  zrng0  17743  mulgghm2OLD  17772  zzngim  17829  zrhpsgnmhm  17858  re0g  17886  pjfval  17975  pjpm  17977  marep01ma  18310  smadiadetlem1a  18313  smadiadetlem3lem2  18317  smadiadetlem3  18318  smadiadetlem4  18319  smadiadet  18320  indistpsALT  18461  tgrest  18607  leordtval2  18660  lmbr2  18707  cnprest  18737  lmff  18749  kgenidm  18964  tx1cn  19026  tx2cn  19027  hausdiag  19062  tsmsresOLD  19561  elrnust  19643  ustbas  19646  ustuqtop0  19659  utopsnneiplem  19666  neipcfilu  19715  psmetge0  19732  xmetge0  19763  qdensere  20193  cnblcld  20198  cnfldms  20199  cnfldtopn  20205  xrsdsre  20231  xrge0tsms  20255  iccpnfcnv  20360  xrhmeo  20362  cnheiborlem  20370  lmmbr2  20614  lmcau  20667  cmetss  20669  cncms  20711  cnfldcusp  20713  ovolctb  20817  ovoliunnul  20834  ismbl  20853  volf  20856  voliunlem1  20875  ioorf  20897  ioorinv  20900  ioorcl  20901  dyaddisj  20920  dyadmax  20922  dyadmbl  20924  mbfid  20958  ismbfd  20962  mbfimaopnlem  20977  limcresi  21204  dvreslem  21228  dvres2lem  21229  dvcjbr  21267  dvferm1  21301  dvferm2  21303  dvlip2  21311  dv11cn  21317  deg1ldg  21450  deg1leb  21453  plycpn  21642  vieta1lem2  21664  elqaa  21675  aalioulem2  21686  aaliou3lem3  21697  aaliou3lem4  21699  pserulm  21774  psercnlem2  21776  psercnlem1  21777  psercn  21778  abelth  21793  reeff1o  21799  pilem1  21803  efhalfpi  21820  coseq0negpitopi  21852  pige3  21866  tanregt0  21882  efif1olem3  21887  efif1olem4  21888  efifo  21890  eff1olem  21891  logrn  21897  ellogrn  21898  relogf1o  21905  argregt0  21946  argrege0  21947  dvrelog  21969  dvloglem  21980  logf1o2  21982  dvlog  21983  efopnlem1  21988  efopnlem2  21989  logtayl  21992  cxpcn3lem  22072  cxpcn3  22073  resqrcn  22074  asinneg  22168  asinrebnd  22183  atan0  22190  atanbnd  22208  areambl  22239  sqrlim  22253  amgmlem  22270  basellem1  22305  basellem4  22308  sqff1o  22407  dchrplusg  22473  bposlem6  22515  bposlem8  22517  dchrvmasumlem2  22634  mulog2sum  22673  pntibndlem1  22725  pntlemo  22743  qrng0  22757  ostth  22775  constr1trl  23312  vdegp1ai  23430  grporn  23524  issubgoi  23622  gidsn  23660  ginvsn  23661  rngomndo  23733  ip0i  24050  ubthlem1  24096  ubthlem2  24097  axhcompl-zf  24225  normlem7  24343  bcseqi  24347  bcsiALT  24406  hlimf  24465  hlimuni  24466  hhshsslem1  24493  hhsssh  24495  hhsscms  24505  occllem  24531  occl  24532  h1deoi  24777  h1dei  24778  h1de2ctlem  24783  h1de2ci  24784  spansni  24785  spanunsni  24807  pjpythi  24950  nmfn0  25216  nmopadjlem  25318  adjcoi  25329  nmopcoadji  25330  pjoccoi  25407  shatomistici  25590  ceqsexv2d  25708  imadifxp  25765  xppreima  25790  1stpreima  25827  2ndpreima  25828  dmct  25840  xrge0neqmnf  25977  rge0srg  26066  gsumpropd2lem  26095  xrge0tsmsd  26108  reofld  26164  rearchi  26166  nn0archi  26167  xrge0slmod  26168  iistmd  26188  xpinpreima  26192  xpinpreima2  26193  tpr2rico  26198  mndpluscn  26212  xrge0pluscn  26226  cnzh  26255  rezh  26256  rrhcn  26282  cnrrext  26295  zrhre  26301  qqhre  26302  sigaex  26408  brsiga  26453  cntnevol  26498  voliune  26501  ddemeas  26508  1stmbfm  26531  2ndmbfm  26532  br2base  26540  dya2icoseg2  26549  dya2iocucvr  26555  eulerpartlemt  26604  eulerpartgbij  26605  eulerpartlemmf  26608  eulerpartlemgvv  26609  eulerpartlemgf  26612  eulerpart  26615  sseqmw  26624  sseqf  26625  sseqp1  26628  fiblem  26631  fibp1  26634  dstrvprob  26704  coinflipspace  26713  coinfliprv  26715  coinflippv  26716  ballotlem1  26719  ballotlem8  26769  lgamucov  26874  iccllyscon  26989  rellyscon  26990  dfrdg2  27458  omsinds  27529  trpredlem1  27540  trpredtr  27543  trpredmintr  27544  wfrlem14  27586  dfrdg4  27830  imagesset  27833  elhf  28061  limsucncmpi  28141  ovoliunnfl  28279  voliunnfl  28281  mbfresfi  28284  dvtanlem  28287  dvtan  28288  itg2addnc  28292  ftc1anclem3  28315  areacirc  28335  filnetlem3  28447  fdc  28487  ismrer1  28583  reheibor  28584  2rexfrabdioph  28981  3rexfrabdioph  28982  4rexfrabdioph  28983  6rexfrabdioph  28984  7rexfrabdioph  28985  rencldnfi  29007  jm2.27dlem2  29206  wepwso  29242  dfac11  29262  pwssplit4  29289  frlmpwfi  29300  isnumbasgrplem3  29308  mpaaeu  29354  proot1mul  29411  proot1hash  29415  seff  29442  sumsnd  29595  stoweidlem34  29677  stoweidlem37  29680  stirlinglem11  29727  stirlinglem12  29728  hashrabsn01  30080  hashrabsn1  30081  abln0  30773  rngn0  30777  lmodn0  30786  zlmodzxzldeplem3  30793  lvecpsslmod  30798  elimhyps  32225  dedths  32226  tendo0co2  34045  erng1r  34252  dvalveclem  34283  dva0g  34285  dvh0g  34369  taupilem3  35225