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  3071  eqvinc  3154  dtru  4592  intasym  5221  relcoi1OLD  5372  funres11  5661  cnvresid  5663  elnn  6721  omsinds  6730  fparlem1  6915  fparlem2  6916  dftpos4  7010  tposf12  7016  wfrlem14  7067  tfr2b  7132  tz7.44lem1  7141  xpcomco  7680  sbthlem2  7701  fidomdm  7871  marypha1lem  7965  hartogslem1  8075  brwdom2  8106  inf3lem6  8156  omex  8166  cnfcom  8223  tz9.1c  8232  r1tr  8265  r1ord3g  8268  rankwflemb  8282  r1elwf  8285  r1elss  8295  rankval3b  8315  onssr1  8320  infxpenlem  8462  alephnbtwn  8520  alephordilem1  8522  alephfp  8557  dfac13  8590  pwsdompw  8652  infcdaabs  8654  ackbij1  8686  ackbij2  8691  r1om  8692  cflim2  8711  fin23lem27  8776  fin23lem29  8789  fin23lem30  8790  fin1a2lem6  8853  fin1a2lem7  8854  fin1a2lem13  8860  itunitc1  8868  itunitc  8869  ituniiun  8870  hsmexlem5  8878  axcc2lem  8884  axcc3  8886  zorn2lem6  8949  zorn2lem7  8950  ttukeylem6  8962  axdc  8969  fodom  8970  iunfo  8982  cardval  8989  cardid  8990  pwcfsdom  9026  alephom  9028  fpwwe  9089  canthp1lem2  9096  canthp1  9097  gchaleph2  9115  r1limwun  9179  inaprc  9279  nqerf  9373  recmulnq  9407  dmrecnq  9411  halfnq  9419  genpdm  9445  reclem3pr  9492  axresscn  9590  axpre-sup  9611  1re  9660  0re  9661  00id  9826  addid1  9831  renegcli  9955  zexALT  10980  uzn0  11198  dfle2  11469  xrinfmss  11620  xrge0neqmnf  11762  axdc4uzlem  12233  facnn  12499  fac0  12500  hashgval  12556  hashinf  12558  hashresfn  12561  hashrabrsn  12589  hashrabsn01  12590  hashrabsn1  12591  hashp1i  12618  hashxplem  12646  fi1uzind  12691  fi1uzindOLD  12697  cshw1  12978  cats1fv  13014  trclubgi  13137  trclubgiOLD  13138  cnrecnv  13305  rexanuz  13485  climdm  13695  lo1eq  13709  rlimeq  13710  sumsn  13884  tanval  14259  rpnnen2lem11  14354  rpnnen  14356  sadadd2lem  14512  sadadd3  14514  sadaddlem  14519  sadasslem  14523  sadeq  14525  lcmgcdlem  14650  3prm  14720  unbenlem  14931  prmreclem6  14944  vdwlem8  15017  vdwnnlem1  15024  0ram  15057  prmgaplcmlem1OLD  15091  prmgaplcmlem2OLD  15092  prmdvdsprmorpOLD  15095  prmgapprmorlemOLD  15096  prmorlelcmfOLD  15099  prmorlelcmsOLDOLD  15101  structcnvcnv  15210  prdsval  15431  prdsbas  15433  prdsplusg  15434  prdsmulr  15435  prdsvsca  15436  prdshom  15443  xpsfrn  15553  xpsff1o2  15555  catcoppccl  16081  catcfuccl  16082  catcxpccl  16170  tsrss  16547  gsumpropd2lem  16594  symgid  17120  mvdco  17164  efgmnvl  17442  efgval  17445  efgi0  17448  efgi1  17449  efgredeu  17480  0frgp  17507  abln0  17583  lt6abl  17607  gsumval3  17619  gsum2dlem2  17681  dprdres  17739  dmdprdsplit2lem  17756  ringn0  17909  isdrng2  18063  drngmcl  18066  drngid2  18069  psrplusg  18682  coe1sfi  18883  ply1plusgfvi  18912  cnfldplusf  19072  cnfldsub  19073  cnsubmlem  19093  cnmsubglem  19107  gzrngunitlem  19109  rge0srg  19115  zring0  19126  zzngim  19200  zrhpsgnmhm  19229  re0g  19257  pjfval  19346  pjpm  19348  marep01ma  19762  smadiadetlem1a  19765  smadiadetlem3lem2  19769  smadiadetlem3  19770  smadiadetlem4  19771  smadiadet  19772  indistpsALT  20105  tgrest  20252  leordtval2  20305  lmbr2  20352  cnprest  20382  lmff  20394  kgenidm  20639  tx1cn  20701  tx2cn  20702  hausdiag  20737  elrnust  21317  ustbas  21320  ustuqtop0  21333  utopsnneiplem  21340  neipcfilu  21389  psmetge0  21406  xmetge0  21437  qdensere  21868  cnblcld  21873  cnfldms  21874  cnfldtopn  21880  xrsdsre  21906  xrge0tsms  21930  iccpnfcnv  22050  xrhmeo  22052  cnheiborlem  22060  lmmbr2  22307  lmcau  22360  cmetss  22362  cncms  22400  cnfldcusp  22402  ovolctb  22521  ovoliunnul  22538  ismbl  22558  volf  22561  voliunlem1  22582  ioorf  22604  ioorinv  22607  ioorcl  22608  ioorfOLD  22609  ioorinvOLD  22612  ioorclOLD  22613  dyaddisj  22633  dyadmax  22635  dyadmbl  22637  mbfid  22671  ismbfd  22675  mbfimaopnlem  22690  limcresi  22919  dvreslem  22943  dvres2lem  22944  dvcjbr  22982  dvferm1  23016  dvferm2  23018  dvlip2  23026  dv11cn  23032  deg1ldg  23120  deg1leb  23123  plycpn  23321  vieta1lem2  23343  elqaa  23357  aalioulem2  23368  aaliou3lem3  23379  aaliou3lem4  23381  pserulm  23456  psercnlem2  23458  psercnlem1  23459  psercn  23460  abelth  23475  reeff1o  23481  pilem1  23485  efhalfpi  23505  coseq0negpitopi  23537  pige3  23551  tanregt0  23567  efif1olem3  23572  efif1olem4  23573  efifo  23575  eff1olem  23576  efsubm  23579  logrn  23587  ellogrn  23588  relogf1o  23595  argregt0  23638  argrege0  23639  dvrelog  23661  dvloglem  23672  logf1o2  23674  dvlog  23675  efopnlem1  23680  efopnlem2  23681  logtayl  23684  cxpcn3lem  23766  cxpcn3  23767  resqrtcn  23768  asinneg  23891  asinrebnd  23906  atan0  23913  atanbnd  23931  areambl  23963  sqrtlim  23977  amgmlem  23994  lgamucov  24042  basellem1  24086  basellem4  24089  sqff1o  24188  dchrplusg  24254  bposlem6  24296  bposlem8  24298  dchrvmasumlem2  24415  mulog2sum  24454  pntibndlem1  24506  pntlemo  24524  qrng0  24538  ostth  24556  lmif  24906  islmib  24908  usgraexmplef  25207  usgraexmpledg  25210  constr1trl  25397  vdegp1ai  25791  grporn  26021  issubgoi  26119  gidsn  26157  ginvsn  26158  efghgrpOLD  26182  rngomndo  26230  ip0i  26547  ubthlem1  26593  ubthlem2  26594  axhcompl-zf  26732  normlem7  26850  bcseqi  26854  bcsiALT  26913  hlimf  26971  hlimuni  26972  hhshsslem1  26999  hhsssh  27001  hhsscms  27011  occllem  27037  occl  27038  h1deoi  27283  h1dei  27284  h1de2ctlem  27289  h1de2ci  27290  spansni  27291  spanunsni  27313  pjpythi  27456  nmfn0  27721  nmopadjlem  27823  adjcoi  27834  nmopcoadji  27835  pjoccoi  27912  shatomistici  28095  imadifxp  28288  idssxp  28303  xppreima  28324  1stpreima  28362  2ndpreima  28363  dmct  28373  gsummpt2d  28618  xrge0tsmsd  28622  reofld  28677  rearchi  28679  nn0archi  28680  xrge0slmod  28681  qtophaus  28737  iistmd  28782  xpinpreima  28786  xpinpreima2  28787  tpr2rico  28792  mndpluscn  28806  xrge0pluscn  28820  cnzh  28848  rezh  28849  qqhucn  28870  rrhcn  28875  cnrrext  28888  zrhre  28897  qqhre  28898  ismntop  28904  sigaex  29005  brsiga  29079  cntnevol  29124  voliune  29125  ddemeas  29132  1stmbfm  29155  2ndmbfm  29156  br2base  29164  dya2icoseg2  29173  dya2iocucvr  29179  carsgclctunlem2  29224  carsgclctunlem3  29225  sitgaddlemb  29254  eulerpartlemt  29277  eulerpartgbij  29278  eulerpartlemmf  29281  eulerpartlemgvv  29282  eulerpartlemgf  29285  eulerpart  29288  sseqmw  29297  sseqf  29298  sseqp1  29301  fiblem  29304  fibp1  29307  dstrvprob  29377  coinflipspace  29386  coinfliprv  29388  coinflippv  29389  ballotlem1  29392  ballotlem8  29442  ballotlem8OLD  29480  iccllyscon  30045  rellyscon  30046  msrid  30255  dfrdg2  30513  trpredlem1  30539  trpredtr  30542  trpredmintr  30543  dfrdg4  30789  imagesset  30791  elhf  31012  filnetlem3  31107  limsucncmpi  31176  taupilem3  31790  icoreresf  31825  icoreelrnab  31827  relowlssretop  31836  poimirlem3  32007  poimirlem9  32013  poimirlem15  32019  poimirlem16  32020  poimirlem17  32021  poimirlem19  32023  poimirlem27  32031  poimirlem28  32032  poimirlem31  32035  poimirlem32  32036  mblfinlem1  32041  ovoliunnfl  32046  voliunnfl  32048  mbfresfi  32051  dvtanlemOLD  32055  dvtan  32056  itg2addnc  32060  ftc1anclem3  32083  areacirc  32101  fdc  32138  ismrer1  32234  reheibor  32235  ac6s6f  32480  elimhyps  32597  dedths  32598  tendo0co2  34426  erng1r  34633  dvalveclem  34664  dva0g  34666  dvh0g  34750  2rexfrabdioph  35710  3rexfrabdioph  35711  4rexfrabdioph  35712  6rexfrabdioph  35713  7rexfrabdioph  35714  rencldnfi  35735  jm2.27dlem2  35936  wepwso  35972  dfac11  35991  pwssplit4  36018  frlmpwfi  36027  isnumbasgrplem3  36035  mpaaeu  36087  proot1mul  36144  proot1hash  36148  cnvcnvintabd  36277  rtrclex  36295  cnvrcl0  36303  dfrtrcl5  36307  frege92  36622  seff  36727  prmunb2  36729  binomcxplemdvbinom  36772  binomcxplemcvg  36773  binomcxplemnotnn0  36775  sumsnd  37410  sumsnf  37744  islptre  37796  stoweidlem34  38007  stoweidlem37  38010  stirlinglem11  38058  stirlinglem12  38059  stirlinglem13  38060  fouriersw  38207  gboge7  39009  nnsum3primes4  39028  structiedg0val  39277  snstriedgval  39291  usgrexmpledg  39498  vtxdlfgrval  39708  upgr2pthnlp  39925  konigsberglem5  40170  2zrng0  40446  lmodn0  40796  zlmodzxzldeplem3  40803  lvecpsslmod  40808  0dig2pr01  40929  aacllem  41046