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  3230  intasym  5382  relcoi1  5536  funres11  5656  cnvresid  5658  elnn  6694  fparlem1  6883  fparlem2  6884  dftpos4  6974  tposf12  6980  tfr2b  7065  tz7.44lem1  7071  xpcomco  7607  sbthlem2  7628  fidomdm  7802  marypha1lem  7893  hartogslem1  7967  brwdom2  7999  inf3lem6  8050  omex  8060  cantnfvalOLD  8117  cnfcom  8144  cnfcomOLD  8152  cnfcom2OLD  8154  cnfcom3lemOLD  8155  cnfcom3OLD  8156  tz9.1c  8161  r1tr  8194  r1ord3g  8197  rankwflemb  8211  r1elwf  8214  r1elss  8224  rankval3b  8244  onssr1  8249  infxpenlem  8391  alephnbtwn  8452  alephordilem1  8454  alephfp  8489  dfac13  8522  pwsdompw  8584  infcdaabs  8586  ackbij1  8618  ackbij2  8623  r1om  8624  cflim2  8643  fin23lem27  8708  fin23lem29  8721  fin23lem30  8722  fin1a2lem6  8785  fin1a2lem7  8786  fin1a2lem13  8792  itunitc1  8800  itunitc  8801  ituniiun  8802  hsmexlem5  8810  axcc2lem  8816  axcc3  8818  zorn2lem6  8881  zorn2lem7  8882  ttukeylem6  8894  axdc  8901  fodom  8902  iunfo  8914  cardval  8921  cardid  8922  pwcfsdom  8958  alephom  8960  fpwwe  9024  canthp1lem2  9031  canthp1  9032  gchaleph2  9050  r1limwun  9114  inaprc  9214  nqerf  9308  recmulnq  9342  dmrecnq  9346  halfnq  9354  genpdm  9380  reclem3pr  9427  axresscn  9525  axpre-sup  9546  1re  9595  0re  9596  00id  9754  addid1  9759  renegcli  9880  zexALT  10883  uzn0  11097  dfle2  11353  xrinfmss  11501  axdc4uzlem  12060  facnn  12323  fac0  12324  hashgval  12376  hashinf  12378  hashresfn  12381  hashrabrsn  12408  hashrabsn01  12409  hashrabsn1  12410  hashp1i  12434  hashxplem  12457  brfi1uzind  12498  cshw1  12753  cats1fv  12787  cnrecnv  12961  rexanuz  13141  climdm  13340  lo1eq  13354  rlimeq  13355  sumsn  13526  tanval  13724  rpnnen2lem11  13819  rpnnen  13821  sadadd2lem  13968  sadadd3  13970  sadaddlem  13975  sadasslem  13979  sadeq  13981  3prm  14093  unbenlem  14285  prmreclem6  14298  vdwlem8  14365  vdwnnlem1  14372  0ram  14397  structcnvcnv  14501  prdsval  14710  prdsbas  14712  prdsplusg  14713  prdsmulr  14714  prdsvsca  14715  prdshom  14722  xpsfrn  14824  xpsff1o2  14826  catcoppccl  15293  catcfuccl  15294  catcxpccl  15334  tsrss  15710  gsumpropd2lem  15827  symgid  16231  mvdco  16276  efgmnvl  16538  efgval  16541  efgi0  16544  efgi1  16545  efgredeu  16576  0frgp  16603  abln0  16676  lt6abl  16700  gsumval3OLD  16711  gsumval3  16714  gsumzresOLD  16721  gsumzaddOLD  16740  gsum2dlem2  16801  gsum2dOLD  16803  dprdfaddOLD  16869  dprdres  16877  dmdprdsplit2lem  16896  rngn0  17050  isdrng2  17206  drngmcl  17209  drngid2  17212  psrplusg  17833  coe1sfi  18051  coe1sfiOLD  18052  ply1plusgfvi  18082  cnfldplusf  18244  cnfldsub  18245  cnsubmlem  18262  cnmsubglem  18276  gzrngunitlem  18278  rge0srg  18283  zring0  18294  zrng0  18300  mulgghm2OLD  18329  zzngim  18386  zrhpsgnmhm  18415  re0g  18443  pjfval  18532  pjpm  18534  marep01ma  18957  smadiadetlem1a  18960  smadiadetlem3lem2  18964  smadiadetlem3  18965  smadiadetlem4  18966  smadiadet  18967  indistpsALT  19308  tgrest  19454  leordtval2  19507  lmbr2  19554  cnprest  19584  lmff  19596  kgenidm  19811  tx1cn  19873  tx2cn  19874  hausdiag  19909  tsmsresOLD  20408  elrnust  20490  ustbas  20493  ustuqtop0  20506  utopsnneiplem  20513  neipcfilu  20562  psmetge0  20579  xmetge0  20610  qdensere  21040  cnblcld  21045  cnfldms  21046  cnfldtopn  21052  xrsdsre  21078  xrge0tsms  21102  iccpnfcnv  21207  xrhmeo  21209  cnheiborlem  21217  lmmbr2  21461  lmcau  21514  cmetss  21516  cncms  21558  cnfldcusp  21560  ovolctb  21664  ovoliunnul  21681  ismbl  21700  volf  21703  voliunlem1  21723  ioorf  21745  ioorinv  21748  ioorcl  21749  dyaddisj  21768  dyadmax  21770  dyadmbl  21772  mbfid  21806  ismbfd  21810  mbfimaopnlem  21825  limcresi  22052  dvreslem  22076  dvres2lem  22077  dvcjbr  22115  dvferm1  22149  dvferm2  22151  dvlip2  22159  dv11cn  22165  deg1ldg  22255  deg1leb  22258  plycpn  22447  vieta1lem2  22469  elqaa  22480  aalioulem2  22491  aaliou3lem3  22502  aaliou3lem4  22504  pserulm  22579  psercnlem2  22581  psercnlem1  22582  psercn  22583  abelth  22598  reeff1o  22604  pilem1  22608  efhalfpi  22625  coseq0negpitopi  22657  pige3  22671  tanregt0  22687  efif1olem3  22692  efif1olem4  22693  efifo  22695  eff1olem  22696  logrn  22702  ellogrn  22703  relogf1o  22710  argregt0  22751  argrege0  22752  dvrelog  22774  dvloglem  22785  logf1o2  22787  dvlog  22788  efopnlem1  22793  efopnlem2  22794  logtayl  22797  cxpcn3lem  22877  cxpcn3  22878  resqrtcn  22879  asinneg  22973  asinrebnd  22988  atan0  22995  atanbnd  23013  areambl  23044  sqrtlim  23058  amgmlem  23075  basellem1  23110  basellem4  23113  sqff1o  23212  dchrplusg  23278  bposlem6  23320  bposlem8  23322  dchrvmasumlem2  23439  mulog2sum  23478  pntibndlem1  23530  pntlemo  23548  qrng0  23562  ostth  23580  lmif  23856  islmib  23858  usgraexmpledg  24107  constr1trl  24294  vdegp1ai  24688  grporn  24918  issubgoi  25016  gidsn  25054  ginvsn  25055  rngomndo  25127  ip0i  25444  ubthlem1  25490  ubthlem2  25491  axhcompl-zf  25619  normlem7  25737  bcseqi  25741  bcsiALT  25800  hlimf  25859  hlimuni  25860  hhshsslem1  25887  hhsssh  25889  hhsscms  25899  occllem  25925  occl  25926  h1deoi  26171  h1dei  26172  h1de2ctlem  26177  h1de2ci  26178  spansni  26179  spanunsni  26201  pjpythi  26344  nmfn0  26610  nmopadjlem  26712  adjcoi  26723  nmopcoadji  26724  pjoccoi  26801  shatomistici  26984  ceqsexv2d  27101  imadifxp  27159  idssxp  27170  xppreima  27187  1stpreima  27224  2ndpreima  27225  dmct  27237  xrge0neqmnf  27369  xrge0tsmsd  27466  reofld  27521  rearchi  27523  nn0archi  27524  xrge0slmod  27525  iistmd  27548  xpinpreima  27552  xpinpreima2  27553  tpr2rico  27558  mndpluscn  27572  xrge0pluscn  27586  cnzh  27615  rezh  27616  rrhcn  27642  cnrrext  27655  zrhre  27661  qqhre  27662  qtophaus  27665  ismntop  27672  sigaex  27777  brsiga  27822  cntnevol  27867  voliune  27869  ddemeas  27876  1stmbfm  27899  2ndmbfm  27900  br2base  27908  dya2icoseg2  27917  dya2iocucvr  27923  eulerpartlemt  27978  eulerpartgbij  27979  eulerpartlemmf  27982  eulerpartlemgvv  27983  eulerpartlemgf  27986  sseqmw  27998  sseqf  27999  sseqp1  28002  fiblem  28005  fibp1  28008  dstrvprob  28078  coinflipspace  28087  coinfliprv  28089  coinflippv  28090  ballotlem1  28093  ballotlem8  28143  lgamucov  28248  iccllyscon  28363  rellyscon  28364  dfrdg2  28833  omsinds  28904  trpredlem1  28915  trpredtr  28918  trpredmintr  28919  wfrlem14  28961  dfrdg4  29205  imagesset  29208  elhf  29436  limsucncmpi  29515  ovoliunnfl  29661  voliunnfl  29663  mbfresfi  29666  dvtanlem  29669  dvtan  29670  itg2addnc  29674  ftc1anclem3  29697  areacirc  29717  filnetlem3  29829  fdc  29869  ismrer1  29965  reheibor  29966  ac6s6f  30213  2rexfrabdioph  30361  3rexfrabdioph  30362  4rexfrabdioph  30363  6rexfrabdioph  30364  7rexfrabdioph  30365  rencldnfi  30387  jm2.27dlem2  30584  wepwso  30620  dfac11  30640  pwssplit4  30667  frlmpwfi  30678  isnumbasgrplem3  30686  mpaaeu  30732  proot1mul  30789  proot1hash  30793  seff  30820  prmunb2  30822  lcmgcdlem  30840  sumsnd  31007  islptre  31189  stoweidlem34  31362  stoweidlem37  31365  stirlinglem11  31412  stirlinglem12  31413  mgmplusgiop  31961  sgrpplusgaop  31962  lmodn0  32195  zlmodzxzldeplem3  32202  lvecpsslmod  32207  elimhyps  33782  dedths  33783  tendo0co2  35602  erng1r  35809  dvalveclem  35840  dva0g  35842  dvh0g  35926  taupilem3  36782