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:  ceqsexv2d  3084  eqvinc  3165  dtru  4593  intasym  5214  relcoi1OLD  5364  funres11  5649  cnvresid  5651  elnn  6699  omsinds  6708  fparlem1  6893  fparlem2  6894  dftpos4  6989  tposf12  6995  wfrlem14  7046  tfr2b  7111  tz7.44lem1  7120  xpcomco  7659  sbthlem2  7680  fidomdm  7850  marypha1lem  7944  hartogslem1  8054  brwdom2  8085  inf3lem6  8135  omex  8145  cnfcom  8202  tz9.1c  8211  r1tr  8244  r1ord3g  8247  rankwflemb  8261  r1elwf  8264  r1elss  8274  rankval3b  8294  onssr1  8299  infxpenlem  8441  alephnbtwn  8499  alephordilem1  8501  alephfp  8536  dfac13  8569  pwsdompw  8631  infcdaabs  8633  ackbij1  8665  ackbij2  8670  r1om  8671  cflim2  8690  fin23lem27  8755  fin23lem29  8768  fin23lem30  8769  fin1a2lem6  8832  fin1a2lem7  8833  fin1a2lem13  8839  itunitc1  8847  itunitc  8848  ituniiun  8849  hsmexlem5  8857  axcc2lem  8863  axcc3  8865  zorn2lem6  8928  zorn2lem7  8929  ttukeylem6  8941  axdc  8948  fodom  8949  iunfo  8961  cardval  8968  cardid  8969  pwcfsdom  9005  alephom  9007  fpwwe  9068  canthp1lem2  9075  canthp1  9076  gchaleph2  9094  r1limwun  9158  inaprc  9258  nqerf  9352  recmulnq  9386  dmrecnq  9390  halfnq  9398  genpdm  9424  reclem3pr  9471  axresscn  9569  axpre-sup  9590  1re  9639  0re  9640  00id  9805  addid1  9810  renegcli  9932  zexALT  10953  uzn0  11171  dfle2  11443  xrinfmss  11592  xrge0neqmnf  11734  axdc4uzlem  12192  facnn  12458  fac0  12459  hashgval  12515  hashinf  12517  hashresfn  12520  hashrabrsn  12548  hashrabsn01  12549  hashrabsn1  12550  hashp1i  12577  hashxplem  12602  fi1uzind  12647  cshw1  12916  cats1fv  12950  trclubgi  13054  cnrecnv  13221  rexanuz  13401  climdm  13611  lo1eq  13625  rlimeq  13626  sumsn  13800  tanval  14175  rpnnen2lem11  14270  rpnnen  14272  sadadd2lem  14426  sadadd3  14428  sadaddlem  14433  sadasslem  14437  sadeq  14439  lcmgcdlem  14564  3prm  14634  unbenlem  14845  prmreclem6  14858  vdwlem8  14931  vdwnnlem1  14938  0ram  14971  prmgaplcmlem1OLD  15005  prmgaplcmlem2OLD  15006  prmdvdsprmorpOLD  15009  prmgapprmorlemOLD  15010  prmorlelcmfOLD  15013  prmorlelcmsOLDOLD  15015  structcnvcnv  15125  prdsval  15346  prdsbas  15348  prdsplusg  15349  prdsmulr  15350  prdsvsca  15351  prdshom  15358  xpsfrn  15468  xpsff1o2  15470  catcoppccl  15996  catcfuccl  15997  catcxpccl  16085  tsrss  16462  gsumpropd2lem  16509  symgid  17035  mvdco  17079  efgmnvl  17357  efgval  17360  efgi0  17363  efgi1  17364  efgredeu  17395  0frgp  17422  abln0  17498  lt6abl  17522  gsumval3  17534  gsum2dlem2  17596  dprdres  17654  dmdprdsplit2lem  17671  ringn0  17824  isdrng2  17978  drngmcl  17981  drngid2  17984  psrplusg  18598  coe1sfi  18799  ply1plusgfvi  18828  cnfldplusf  18988  cnfldsub  18989  cnsubmlem  19009  cnmsubglem  19023  gzrngunitlem  19025  rge0srg  19031  zring0  19042  zzngim  19116  zrhpsgnmhm  19145  re0g  19173  pjfval  19262  pjpm  19264  marep01ma  19678  smadiadetlem1a  19681  smadiadetlem3lem2  19685  smadiadetlem3  19686  smadiadetlem4  19687  smadiadet  19688  indistpsALT  20021  tgrest  20168  leordtval2  20221  lmbr2  20268  cnprest  20298  lmff  20310  kgenidm  20555  tx1cn  20617  tx2cn  20618  hausdiag  20653  elrnust  21232  ustbas  21235  ustuqtop0  21248  utopsnneiplem  21255  neipcfilu  21304  psmetge0  21321  xmetge0  21352  qdensere  21783  cnblcld  21788  cnfldms  21789  cnfldtopn  21795  xrsdsre  21821  xrge0tsms  21845  iccpnfcnv  21965  xrhmeo  21967  cnheiborlem  21975  lmmbr2  22222  lmcau  22275  cmetss  22277  cncms  22315  cnfldcusp  22317  ovolctb  22436  ovoliunnul  22453  ismbl  22473  volf  22476  voliunlem1  22496  ioorf  22518  ioorinv  22521  ioorcl  22522  ioorfOLD  22523  ioorinvOLD  22526  ioorclOLD  22527  dyaddisj  22547  dyadmax  22549  dyadmbl  22551  mbfid  22585  ismbfd  22589  mbfimaopnlem  22604  limcresi  22833  dvreslem  22857  dvres2lem  22858  dvcjbr  22896  dvferm1  22930  dvferm2  22932  dvlip2  22940  dv11cn  22946  deg1ldg  23034  deg1leb  23037  plycpn  23235  vieta1lem2  23257  elqaa  23271  aalioulem2  23282  aaliou3lem3  23293  aaliou3lem4  23295  pserulm  23370  psercnlem2  23372  psercnlem1  23373  psercn  23374  abelth  23389  reeff1o  23395  pilem1  23399  efhalfpi  23419  coseq0negpitopi  23451  pige3  23465  tanregt0  23481  efif1olem3  23486  efif1olem4  23487  efifo  23489  eff1olem  23490  efsubm  23493  logrn  23501  ellogrn  23502  relogf1o  23509  argregt0  23552  argrege0  23553  dvrelog  23575  dvloglem  23586  logf1o2  23588  dvlog  23589  efopnlem1  23594  efopnlem2  23595  logtayl  23598  cxpcn3lem  23680  cxpcn3  23681  resqrtcn  23682  asinneg  23805  asinrebnd  23820  atan0  23827  atanbnd  23845  areambl  23877  sqrtlim  23891  amgmlem  23908  lgamucov  23956  basellem1  24000  basellem4  24003  sqff1o  24102  dchrplusg  24168  bposlem6  24210  bposlem8  24212  dchrvmasumlem2  24329  mulog2sum  24368  pntibndlem1  24420  pntlemo  24438  qrng0  24452  ostth  24470  lmif  24820  islmib  24822  usgraexmplef  25121  usgraexmpledg  25124  constr1trl  25311  vdegp1ai  25705  grporn  25933  issubgoi  26031  gidsn  26069  ginvsn  26070  efghgrpOLD  26094  rngomndo  26142  ip0i  26459  ubthlem1  26505  ubthlem2  26506  axhcompl-zf  26644  normlem7  26762  bcseqi  26766  bcsiALT  26825  hlimf  26883  hlimuni  26884  hhshsslem1  26911  hhsssh  26913  hhsscms  26923  occllem  26949  occl  26950  h1deoi  27195  h1dei  27196  h1de2ctlem  27201  h1de2ci  27202  spansni  27203  spanunsni  27225  pjpythi  27368  nmfn0  27633  nmopadjlem  27735  adjcoi  27746  nmopcoadji  27747  pjoccoi  27824  shatomistici  28007  imadifxp  28205  idssxp  28220  xppreima  28241  1stpreima  28280  2ndpreima  28281  dmct  28291  gsummpt2d  28537  xrge0tsmsd  28541  reofld  28596  rearchi  28598  nn0archi  28599  xrge0slmod  28600  qtophaus  28656  iistmd  28701  xpinpreima  28705  xpinpreima2  28706  tpr2rico  28711  mndpluscn  28725  xrge0pluscn  28739  cnzh  28767  rezh  28768  qqhucn  28789  rrhcn  28794  cnrrext  28807  zrhre  28816  qqhre  28817  ismntop  28823  sigaex  28924  brsiga  28998  cntnevol  29043  voliune  29045  ddemeas  29052  1stmbfm  29075  2ndmbfm  29076  br2base  29084  dya2icoseg2  29093  dya2iocucvr  29099  carsgclctunlem2  29144  carsgclctunlem3  29145  sitgaddlemb  29174  eulerpartlemt  29197  eulerpartgbij  29198  eulerpartlemmf  29201  eulerpartlemgvv  29202  eulerpartlemgf  29205  eulerpart  29208  sseqmw  29217  sseqf  29218  sseqp1  29221  fiblem  29224  fibp1  29227  dstrvprob  29297  coinflipspace  29306  coinfliprv  29308  coinflippv  29309  ballotlem1  29312  ballotlem8  29362  ballotlem8OLD  29400  iccllyscon  29966  rellyscon  29967  msrid  30176  dfrdg2  30435  trpredlem1  30461  trpredtr  30464  trpredmintr  30465  dfrdg4  30711  imagesset  30713  elhf  30934  filnetlem3  31029  limsucncmpi  31098  taupilem3  31713  icoreresf  31748  icoreelrnab  31750  relowlssretop  31759  poimirlem3  31936  poimirlem9  31942  poimirlem15  31948  poimirlem16  31949  poimirlem17  31950  poimirlem19  31952  poimirlem27  31960  poimirlem28  31961  poimirlem31  31964  poimirlem32  31965  mblfinlem1  31970  ovoliunnfl  31975  voliunnfl  31977  mbfresfi  31980  dvtanlemOLD  31984  dvtan  31985  itg2addnc  31989  ftc1anclem3  32012  areacirc  32030  fdc  32067  ismrer1  32163  reheibor  32164  ac6s6f  32409  elimhyps  32527  dedths  32528  tendo0co2  34349  erng1r  34556  dvalveclem  34587  dva0g  34589  dvh0g  34673  2rexfrabdioph  35633  3rexfrabdioph  35634  4rexfrabdioph  35635  6rexfrabdioph  35636  7rexfrabdioph  35637  rencldnfi  35658  jm2.27dlem2  35859  wepwso  35895  dfac11  35914  pwssplit4  35941  frlmpwfi  35950  isnumbasgrplem3  35958  mpaaeu  36010  proot1mul  36067  proot1hash  36071  cnvcnvintabd  36200  rtrclex  36218  cnvrcl0  36226  dfrtrcl5  36230  frege92  36545  seff  36651  prmunb2  36653  binomcxplemdvbinom  36696  binomcxplemcvg  36697  binomcxplemnotnn0  36699  sumsnd  37341  sumsnf  37642  islptre  37693  stoweidlem34  37889  stoweidlem37  37892  stirlinglem11  37940  stirlinglem12  37941  stirlinglem13  37942  fouriersw  38089  gboge7  38858  nnsum3primes4  38877  structiedg0val  39110  snstriedgval  39124  usgrexmpledg  39317  vtxdumgrval  39523  2zrng0  39925  lmodn0  40275  zlmodzxzldeplem3  40282  lvecpsslmod  40287  0dig2pr01  40408  aacllem  40527