Theorem mp2b 10

Description: A double modus ponens inference. (Contributed by Mario Carneiro, 24-Jan-2013.)

Hypotheses

Ref	Expression
mp2b.1	⊢ 𝜑
mp2b.2	⊢ (𝜑 → 𝜓)
mp2b.3	⊢ (𝜓 → 𝜒)

Assertion

Ref	Expression
mp2b	⊢ 𝜒

Proof of Theorem mp2b

Step	Hyp	Ref	Expression
1		mp2b.1	. . 3 ⊢ 𝜑
2		mp2b.2	. . 3 ⊢ (𝜑 → 𝜓)
3	1, 2	ax-mp 5	. 2 ⊢ 𝜓
4		mp2b.3	. 2 ⊢ (𝜓 → 𝜒)
5	3, 4	ax-mp 5	1 ⊢ 𝜒

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5

This theorem is referenced by:  minimp-syllsimp  1625  nfcriOLD  2898  nfcriOLDOLD  2899  ceqsexv2d  3482  dtruALT2  5294  dtru  5360  intasym  6025  relcoi2  6184  funres11  6518  cnvresid  6520  omsindsOLD  7743  find  7752  fparlem1  7961  fparlem2  7962  dftpos4  8070  tposf12  8076  wfrlem14OLD  8162  tfr2b  8236  tz7.44lem1  8245  xp01disjl  8331  xpcomco  8858  sbthlem2  8880  fidomdm  9105  brwdom2  9341  epnsym  9376  inf3lem6  9400  omex  9410  cnfcom  9467  ttrclco  9485  ttrclselem2  9493  tz9.1c  9497  frr1  9526  r1tr  9543  r1ord3g  9546  rankwflemb  9560  r1elwf  9563  r1elss  9573  rankval3b  9593  onssr1  9598  inlresf  9681  inrresf  9683  djuin  9685  infxpenlem  9778  alephnbtwn  9836  alephordilem1  9838  alephfp  9873  dfac13  9907  pwsdompw  9969  infdjuabs  9971  ackbij1  10003  ackbij2  10008  r1om  10009  cflim2  10028  fin23lem27  10093  fin23lem29  10106  fin23lem30  10107  fin1a2lem6  10170  fin1a2lem7  10171  fin1a2lem13  10177  itunitc1  10185  itunitc  10186  ituniiun  10187  hsmexlem5  10195  axcc2lem  10201  axcc3  10203  zorn2lem6  10266  zorn2lem7  10267  ttukeylem6  10279  axdc  10286  dmct  10289  iunfo  10304  cardval  10311  cardid  10312  pwcfsdom  10348  alephom  10350  canthp1lem2  10418  gchaleph2  10437  r1limwun  10501  inaprc  10601  nqerf  10695  recmulnq  10729  dmrecnq  10733  halfnq  10741  genpdm  10767  reclem3pr  10814  axresscn  10913  axpre-sup  10934  1re  10984  0re  10986  00id  11159  addid1  11164  0cnALT  11218  renegcli  11291  zexALT  12348  uzn0  12608  xrinfmss  13053  axdc4uzlem  13712  facnn  13998  fac0  13999  hashgval  14056  hashinf  14058  hashresfn  14063  hashrabrsn  14096  hashrabsn01  14097  hashrabsn1  14098  hashp1i  14127  hash1snb  14143  hashxplem  14157  fi1uzind  14220  cshw1  14544  cats1fv  14581  trclubgi  14717  cnrecnv  14885  rexanuz  15066  climdm  15272  lo1eq  15286  rlimeq  15287  sumsnf  15464  tanval  15846  rpnnen2lem11  15942  rpnnen  15945  sadadd2lem  16175  sadadd3  16177  sadaddlem  16182  sadasslem  16186  sadeq  16188  lcmgcdlem  16320  unbenlem  16618  prmreclem6  16631  vdwlem8  16698  vdwnnlem1  16705  0ram  16730  structcnvcnv  16863  prdsvallem  17174  prdsval  17175  prdsbas  17177  prdsplusg  17178  prdsmulr  17179  prdsvsca  17180  prdshom  17187  xpsfrn  17288  xpsff1o2  17289  catcoppccl  17841  catcoppcclOLD  17842  catcfuccl  17843  catcfucclOLD  17844  catcxpccl  17933  catcxpcclOLD  17934  tsrss  18316  gsumpropd2lem  18372  smndex2dnrinv  18563  mvdco  19062  efgmnvl  19329  efgval  19332  efgi0  19335  efgi1  19336  efgredeu  19367  0frgp  19394  abln0  19477  lt6abl  19505  gsumval3  19517  gsum2dlem2  19581  dprdres  19640  dmdprdsplit2lem  19657  ringn0  19851  isdrng2  20010  drngmcl  20013  drngid2  20016  cnfldplusf  20634  cnfldsub  20635  cnsubmlem  20655  cnsubglem  20656  cnmsubglem  20670  gzrngunitlem  20672  rge0srg  20678  zring0  20689  zzngim  20769  zrhpsgnmhm  20798  re0g  20826  pjfval  20922  pjpm  20924  psrplusg  21159  coe1sfi  21393  ply1plusgfvi  21422  marep01ma  21818  smadiadetlem1a  21821  smadiadetlem3lem2  21825  smadiadetlem3  21826  smadiadetlem4  21827  smadiadet  21828  indistpsALT  22172  indistpsALTOLD  22173  tgrest  22319  leordtval2  22372  lmbr2  22419  cnprest  22449  lmff  22461  kgenidm  22707  tx1cn  22769  tx2cn  22770  elrnust  23385  ustbas  23388  psmetge0  23474  xmetge0  23506  qdensere  23942  cnblcld  23947  cnfldms  23948  cnfldtopn  23954  xrsdsre  23982  xrge0tsms  24006  iccpnfcnv  24116  xrhmeo  24118  cnheiborlem  24126  cnlmod  24312  recvs  24318  lmmbr2  24432  lmcau  24486  metsscmetcld  24488  cncms  24528  cnfldcusp  24530  ovolctb  24663  ovoliunnul  24680  ismbl  24699  volf  24702  voliunlem1  24723  ioorf  24746  ioorinv  24749  ioorcl  24750  dyaddisj  24769  dyadmax  24771  dyadmbl  24773  mbfid  24808  ismbfd  24812  mbfimaopnlem  24828  limcresi  25058  dvreslem  25082  dvres2lem  25083  dvcjbr  25122  dvferm1  25158  dvferm2  25160  dvlip2  25168  dv11cn  25174  deg1ldg  25266  deg1leb  25269  plycpn  25458  vieta1lem2  25480  elqaa  25491  aalioulem2  25502  aaliou3lem3  25513  aaliou3lem4  25515  pserulm  25590  psercnlem2  25592  psercnlem1  25593  psercn  25594  abelth  25609  reeff1o  25615  pilem1  25619  efhalfpi  25637  coseq0negpitopi  25669  pige3ALT  25685  tanregt0  25704  efif1olem3  25709  efif1olem4  25710  efifo  25712  eff1olem  25713  efsubm  25716  logrn  25723  ellogrn  25724  relogf1o  25731  argregt0  25774  argrege0  25775  dvrelog  25801  dvloglem  25812  logf1o2  25814  dvlog  25815  efopnlem1  25820  efopnlem2  25821  logtayl  25824  cxpcn3lem  25909  cxpcn3  25910  resqrtcn  25911  asinneg  26045  asinrebnd  26060  atan0  26067  atanbnd  26085  areambl  26117  sqrtlim  26131  amgmlem  26148  lgamucov  26196  basellem1  26239  basellem4  26242  sqff1o  26340  dchrplusg  26404  bposlem6  26446  bposlem8  26448  dchrvmasumlem2  26655  mulog2sum  26694  pntibndlem1  26746  pntlemo  26764  qrng0  26778  ostth  26796  lmif  27155  islmib  27157  structiedg0val  27401  snstriedgval  27417  umgredgnlp  27526  usgrexmplef  27635  usgrexmpledg  27638  vtxdlfgrval  27861  upgr2pthnlp  28109  konigsberglem5  28629  ex-mod  28822  pliguhgr  28857  grporn  28892  ip0i  29196  ubthlem1  29241  ubthlem2  29242  axhcompl-zf  29369  normlem7  29487  bcseqi  29491  bcsiALT  29550  hlimf  29608  hlimuni  29609  hhssabloilem  29632  hhshsslem1  29638  hhsssh  29640  hhsscms  29649  occllem  29674  occl  29675  h1deoi  29920  h1dei  29921  h1de2ctlem  29926  h1de2ci  29927  spansni  29928  spanunsni  29950  pjpythi  30093  nmfn0  30358  nmopadjlem  30460  adjcoi  30471  nmopcoadji  30472  pjoccoi  30549  shatomistici  30732  iuninc  30909  imadifxp  30949  xppreima  30992  1stpreima  31048  2ndpreima  31049  fsuppcurry1  31069  fsuppcurry2  31070  hashgt1  31137  s3clhash  31231  gsummpt2d  31318  xrge0tsmsd  31326  tocyc01  31394  cyc3evpm  31426  cycpmconjslem2  31431  cyc3conja  31433  reofld  31553  rearchi  31555  nn0archi  31556  xrge0slmod  31557  elrspunidl  31615  dimval  31695  dimvalfi  31696  qtophaus  31795  iistmd  31861  xpinpreima  31865  xpinpreima2  31866  tpr2rico  31871  mndpluscn  31885  xrge0pluscn  31899  cnzh  31929  rezh  31930  qqhucn  31951  rrhcn  31956  cnrrext  31969  zrhre  31978  qqhre  31979  ismntop  31985  sigaex  32087  brsiga  32160  cntnevol  32205  voliune  32206  ddemeas  32213  1stmbfm  32236  2ndmbfm  32237  br2base  32245  dya2icoseg2  32254  dya2iocucvr  32260  carsgclctunlem2  32295  carsgclctunlem3  32296  sitgaddlemb  32324  eulerpartlemt  32347  eulerpartgbij  32348  eulerpartlemmf  32351  eulerpartlemgvv  32352  eulerpartlemgf  32355  eulerpart  32358  sseqmw  32367  sseqf  32368  sseqp1  32371  fiblem  32374  fibp1  32377  dstrvprob  32447  coinflipspace  32456  coinfliprv  32458  coinflippv  32459  ballotlem1  32462  ballotlem8  32512  circlemethhgt  32632  usgrcyclgt2v  33102  iccllysconn  33221  rellysconn  33222  satf00  33345  fmla0  33353  msrid  33516  dfrdg2  33780  on2recsfn  33835  on2recsov  33836  on2ind  33837  on3ind  33838  noextendseq  33879  bday0s  34031  oldlim  34078  dfrdg4  34262  imagesset  34264  elhf  34485  filnetlem3  34578  limsucncmpi  34643  bj-babygodel  34794  bj-idres  35340  taupilem3  35499  icoreresf  35532  icoreelrnab  35534  relowlssretop  35543  poimirlem3  35789  poimirlem9  35795  poimirlem15  35801  poimirlem16  35802  poimirlem17  35803  poimirlem19  35805  poimirlem27  35813  poimirlem28  35814  poimirlem31  35817  poimirlem32  35818  mblfinlem1  35823  ovoliunnfl  35828  voliunnfl  35830  mbfresfi  35832  dvtan  35836  itg2addnc  35840  ftc1anclem3  35861  areacirc  35879  fdc  35912  ismrer1  36005  reheibor  36006  rngomndo  36102  gidsn  36119  ac6s6f  36340  eccnvepex  36477  dfcnvrefrels2  36651  dfcnvrefrels3  36652  dedths  36983  tendo0co2  38809  erng1r  39016  dvalveclem  39046  dva0g  39048  dvh0g  39132  sn-dtru  40195  sn-it0e0  40404  sn-0tie0  40428  2rexfrabdioph  40625  3rexfrabdioph  40626  4rexfrabdioph  40627  6rexfrabdioph  40628  7rexfrabdioph  40629  rencldnfi  40650  jm2.27dlem2  40839  wepwso  40875  dfac11  40894  pwssplit4  40921  frlmpwfi  40930  isnumbasgrplem3  40937  mpaaeu  40982  proot1mul  41031  proot1hash  41032  cnvcnvintabd  41215  cnvrcl0  41240  dfrtrcl5  41244  cotrcltrcl  41340  frege92  41570  seff  41934  prmunb2  41936  binomcxplemdvbinom  41978  binomcxplemcvg  41979  binomcxplemnotnn0  41981  sumsnd  42576  islptre  43167  stoweidlem34  43582  stoweidlem37  43585  stirlinglem11  43632  stirlinglem12  43633  stirlinglem13  43634  fouriersw  43779  fundcmpsurbijinjpreimafv  44870  fundcmpsurinjimaid  44874  fmtnoinf  44999  gbowge7  45226  nnsum3primes4  45251  2zrng0  45507  lmodn0  45847  zlmodzxzldeplem3  45854  lvecpsslmod  45859  0dig2pr01  45967  aacllem  46516  amgmwlem  46517  natlocalincr  46522  upwordsing  46530