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  1624  nfcriOLD  2892  nfcriOLDOLD  2893  ceqsexv2d  3498  dtruALT2  5330  dtruOLD  5403  intasym  6074  relcoi2  6234  funres11  6583  cnvresid  6585  omsindsOLD  7829  find  7838  fparlem1  8049  fparlem2  8050  dftpos4  8181  tposf12  8187  wfrlem14OLD  8273  tfr2b  8347  tz7.44lem1  8356  ord3  8434  xp01disjl  8443  on2recsfn  8618  on2recsov  8619  on2ind  8620  on3ind  8621  xpcomco  9013  sbthlem2  9035  fidomdm  9280  brwdom2  9518  epnsym  9554  inf3lem6  9578  omex  9588  cnfcom  9645  ttrclco  9663  ttrclselem2  9671  tz9.1c  9675  frr1  9704  r1tr  9721  r1ord3g  9724  rankwflemb  9738  r1elwf  9741  r1elss  9751  rankval3b  9771  onssr1  9776  inlresf  9859  inrresf  9861  djuin  9863  infxpenlem  9958  alephnbtwn  10016  alephordilem1  10018  alephfp  10053  dfac13  10087  pwsdompw  10149  infdjuabs  10151  ackbij1  10183  ackbij2  10188  r1om  10189  cflim2  10208  fin23lem27  10273  fin23lem29  10286  fin23lem30  10287  fin1a2lem6  10350  fin1a2lem7  10351  fin1a2lem13  10357  itunitc1  10365  itunitc  10366  ituniiun  10367  hsmexlem5  10375  axcc2lem  10381  axcc3  10383  zorn2lem6  10446  zorn2lem7  10447  ttukeylem6  10459  axdc  10466  dmct  10469  iunfo  10484  cardval  10491  cardid  10492  pwcfsdom  10528  alephom  10530  canthp1lem2  10598  gchaleph2  10617  r1limwun  10681  inaprc  10781  nqerf  10875  recmulnq  10909  dmrecnq  10913  halfnq  10921  genpdm  10947  reclem3pr  10994  axresscn  11093  axpre-sup  11114  1re  11164  0re  11166  00id  11339  addrid  11344  0cnALT  11398  renegcli  11471  zexALT  12528  uzn0  12789  xrinfmss  13239  axdc4uzlem  13898  facnn  14185  fac0  14186  hashgval  14243  hashinf  14245  hashresfn  14250  hashrabrsn  14282  hashrabsn01  14283  hashrabsn1  14284  hashp1i  14313  hash1snb  14329  hashxplem  14343  fi1uzind  14408  cshw1  14722  cats1fv  14760  trclubgi  14894  cnrecnv  15062  rexanuz  15242  climdm  15448  lo1eq  15462  rlimeq  15463  sumsnf  15639  tanval  16021  rpnnen2lem11  16117  rpnnen  16120  sadadd2lem  16350  sadadd3  16352  sadaddlem  16357  sadasslem  16361  sadeq  16363  lcmgcdlem  16493  unbenlem  16791  prmreclem6  16804  vdwlem8  16871  vdwnnlem1  16878  0ram  16903  structcnvcnv  17036  prdsvallem  17350  prdsval  17351  prdsbas  17353  prdsplusg  17354  prdsmulr  17355  prdsvsca  17356  prdshom  17363  xpsfrn  17464  xpsff1o2  17465  catcoppccl  18017  catcoppcclOLD  18018  catcfuccl  18019  catcfucclOLD  18020  catcxpccl  18109  catcxpcclOLD  18110  tsrss  18492  gsumpropd2lem  18548  smndex2dnrinv  18739  mvdco  19241  efgmnvl  19510  efgval  19513  efgi0  19516  efgi1  19517  efgredeu  19548  0frgp  19575  abln0  19659  lt6abl  19686  gsumval3  19698  gsum2dlem2  19762  dprdres  19821  dmdprdsplit2lem  19838  ringn0  20041  isdrng2  20238  drngmcl  20241  drngid2  20245  cnfldplusf  20861  cnfldsub  20862  cnsubmlem  20882  cnsubglem  20883  cnmsubglem  20897  gzrngunitlem  20899  rge0srg  20905  zring0  20916  zzngim  20996  zrhpsgnmhm  21025  re0g  21053  pjfval  21149  pjpm  21151  psrplusg  21386  coe1sfi  21621  ply1plusgfvi  21650  marep01ma  22046  smadiadetlem1a  22049  smadiadetlem3lem2  22053  smadiadetlem3  22054  smadiadetlem4  22055  smadiadet  22056  indistpsALT  22400  indistpsALTOLD  22401  tgrest  22547  leordtval2  22600  lmbr2  22647  cnprest  22677  lmff  22689  kgenidm  22935  tx1cn  22997  tx2cn  22998  ustbas  23616  psmetge0  23702  xmetge0  23734  qdensere  24170  cnblcld  24175  cnfldms  24176  cnfldtopn  24182  xrsdsre  24210  xrge0tsms  24234  iccpnfcnv  24344  xrhmeo  24346  cnheiborlem  24354  cnlmod  24540  recvs  24546  lmmbr2  24660  lmcau  24714  metsscmetcld  24716  cncms  24756  cnfldcusp  24758  ovolctb  24891  ovoliunnul  24908  ismbl  24927  volf  24930  voliunlem1  24951  ioorf  24974  ioorinv  24977  ioorcl  24978  dyaddisj  24997  dyadmax  24999  dyadmbl  25001  mbfid  25036  ismbfd  25040  mbfimaopnlem  25056  limcresi  25286  dvreslem  25310  dvres2lem  25311  dvcjbr  25350  dvferm1  25386  dvferm2  25388  dvlip2  25396  dv11cn  25402  deg1ldg  25494  deg1leb  25497  plycpn  25686  vieta1lem2  25708  elqaa  25719  aalioulem2  25730  aaliou3lem3  25741  aaliou3lem4  25743  pserulm  25818  psercnlem2  25820  psercnlem1  25821  psercn  25822  abelth  25837  reeff1o  25843  pilem1  25847  efhalfpi  25865  coseq0negpitopi  25897  pige3ALT  25913  tanregt0  25932  efif1olem3  25937  efif1olem4  25938  efifo  25940  eff1olem  25941  efsubm  25944  logrn  25951  ellogrn  25952  relogf1o  25959  argregt0  26002  argrege0  26003  dvrelog  26029  dvloglem  26040  logf1o2  26042  dvlog  26043  efopnlem1  26048  efopnlem2  26049  logtayl  26052  cxpcn3lem  26137  cxpcn3  26138  resqrtcn  26139  asinneg  26273  asinrebnd  26288  atan0  26295  atanbnd  26313  areambl  26345  sqrtlim  26359  amgmlem  26376  lgamucov  26424  basellem1  26467  basellem4  26470  sqff1o  26568  dchrplusg  26632  bposlem6  26674  bposlem8  26676  dchrvmasumlem2  26883  mulog2sum  26922  pntibndlem1  26974  pntlemo  26992  qrng0  27006  ostth  27024  noextendseq  27052  bday0s  27210  oldlim  27259  lmif  27790  islmib  27792  structiedg0val  28036  snstriedgval  28052  umgredgnlp  28161  usgrexmplef  28270  usgrexmpledg  28273  vtxdlfgrval  28496  upgr2pthnlp  28743  konigsberglem5  29263  ex-mod  29456  pliguhgr  29491  grporn  29526  ip0i  29830  ubthlem1  29875  ubthlem2  29876  axhcompl-zf  30003  normlem7  30121  bcseqi  30125  bcsiALT  30184  hlimf  30242  hlimuni  30243  hhssabloilem  30266  hhshsslem1  30272  hhsssh  30274  hhsscms  30283  occllem  30308  occl  30309  h1deoi  30554  h1dei  30555  h1de2ctlem  30560  h1de2ci  30561  spansni  30562  spanunsni  30584  pjpythi  30727  nmfn0  30992  nmopadjlem  31094  adjcoi  31105  nmopcoadji  31106  pjoccoi  31183  shatomistici  31366  iuninc  31546  imadifxp  31586  xppreima  31629  1stpreima  31688  2ndpreima  31689  fsuppcurry1  31710  fsuppcurry2  31711  hashgt1  31780  s3clhash  31874  gsummpt2d  31961  xrge0tsmsd  31969  tocyc01  32037  cyc3evpm  32069  cycpmconjslem2  32074  cyc3conja  32076  reofld  32207  rearchi  32209  nn0archi  32210  xrge0slmod  32211  elrspunidl  32279  dimval  32384  dimvalfi  32385  ply1degltdimlem  32404  qtophaus  32506  iistmd  32572  xpinpreima  32576  xpinpreima2  32577  tpr2rico  32582  mndpluscn  32596  xrge0pluscn  32610  cnzh  32640  rezh  32641  qqhucn  32662  rrhcn  32667  cnrrext  32680  zrhre  32689  qqhre  32690  ismntop  32696  sigaex  32798  brsiga  32871  cntnevol  32916  voliune  32917  ddemeas  32924  1stmbfm  32949  2ndmbfm  32950  br2base  32958  dya2icoseg2  32967  dya2iocucvr  32973  carsgclctunlem2  33008  carsgclctunlem3  33009  sitgaddlemb  33037  eulerpartlemt  33060  eulerpartgbij  33061  eulerpartlemmf  33064  eulerpartlemgvv  33065  eulerpartlemgf  33068  eulerpart  33071  sseqmw  33080  sseqf  33081  sseqp1  33084  fiblem  33087  fibp1  33090  dstrvprob  33160  coinflipspace  33169  coinfliprv  33171  coinflippv  33172  ballotlem1  33175  ballotlem8  33225  circlemethhgt  33345  usgrcyclgt2v  33812  iccllysconn  33931  rellysconn  33932  satf00  34055  fmla0  34063  msrid  34226  dfrdg2  34456  dfrdg4  34612  imagesset  34614  elhf  34835  filnetlem3  34928  limsucncmpi  34993  bj-babygodel  35144  bj-idres  35704  taupilem3  35863  icoreresf  35896  icoreelrnab  35898  relowlssretop  35907  poimirlem3  36154  poimirlem9  36160  poimirlem15  36166  poimirlem16  36167  poimirlem17  36168  poimirlem19  36170  poimirlem27  36178  poimirlem28  36179  poimirlem31  36182  poimirlem32  36183  mblfinlem1  36188  ovoliunnfl  36193  voliunnfl  36195  mbfresfi  36197  dvtan  36201  itg2addnc  36205  ftc1anclem3  36226  areacirc  36244  fdc  36277  ismrer1  36370  reheibor  36371  rngomndo  36467  gidsn  36484  ac6s6f  36705  eccnvepex  36869  cnvref4  36884  dfcnvrefrels2  37063  dfcnvrefrels3  37064  dedths  37497  tendo0co2  39324  erng1r  39531  dvalveclem  39561  dva0g  39563  dvh0g  39647  sn-it0e0  40942  sn-0tie0  40966  2rexfrabdioph  41177  3rexfrabdioph  41178  4rexfrabdioph  41179  6rexfrabdioph  41180  7rexfrabdioph  41181  rencldnfi  41202  jm2.27dlem2  41392  wepwso  41428  dfac11  41447  pwssplit4  41474  frlmpwfi  41483  isnumbasgrplem3  41490  mpaaeu  41535  proot1mul  41584  proot1hash  41585  epirron  41646  oneptr  41647  ordeldif1o  41653  oaomoencom  41710  oenassex  41711  cnvcnvintabd  41994  cnvrcl0  42019  dfrtrcl5  42023  cotrcltrcl  42119  frege92  42349  seff  42711  prmunb2  42713  binomcxplemdvbinom  42755  binomcxplemcvg  42756  binomcxplemnotnn0  42758  sumsnd  43353  islptre  43980  stoweidlem34  44395  stoweidlem37  44398  stirlinglem11  44445  stirlinglem12  44446  stirlinglem13  44447  fouriersw  44592  natlocalincr  45235  upwordsing  45243  fundcmpsurbijinjpreimafv  45719  fundcmpsurinjimaid  45723  fmtnoinf  45848  gbowge7  46075  nnsum3primes4  46100  2zrng0  46356  lmodn0  46696  zlmodzxzldeplem3  46703  lvecpsslmod  46708  0dig2pr01  46816  aacllem  47368  amgmwlem  47369