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  1623  ceqsexv2dOLD  3489  dtruALT2  5308  intasym  6062  relcoi2  6224  funres11  6558  cnvresid  6560  find  7825  fparlem1  8042  fparlem2  8043  dftpos4  8175  tposf12  8181  tfr2b  8315  tz7.44lem1  8324  ord3  8400  xp01disjl  8407  on2recsfn  8582  on2recsov  8583  on2ind  8584  on3ind  8585  xpcomco  8980  sbthlem2  9001  fidomdm  9218  brwdom2  9459  epnsym  9499  inf3lem6  9523  cnfcom  9590  ttrclco  9608  ttrclselem2  9616  tz9.1c  9620  frr1  9649  r1tr  9666  r1ord3g  9669  rankwflemb  9683  r1elwf  9686  r1elss  9696  rankval3b  9716  onssr1  9721  inlresf  9804  inrresf  9806  djuin  9808  infxpenlem  9901  alephnbtwn  9959  alephordilem1  9961  alephfp  9996  dfac13  10031  pwsdompw  10091  infdjuabs  10093  ackbij1  10125  ackbij2  10130  r1om  10131  cflim2  10151  fin23lem27  10216  fin23lem29  10229  fin23lem30  10230  fin1a2lem6  10293  fin1a2lem7  10294  fin1a2lem13  10300  itunitc1  10308  itunitc  10309  ituniiun  10310  hsmexlem5  10318  axcc2lem  10324  axcc3  10326  zorn2lem6  10389  zorn2lem7  10390  ttukeylem6  10402  dmct  10412  iunfo  10427  cardval  10434  cardid  10435  alephom  10473  canthp1lem2  10541  gchaleph2  10560  r1limwun  10624  inaprc  10724  nqerf  10818  recmulnq  10852  dmrecnq  10856  halfnq  10864  genpdm  10890  reclem3pr  10937  axresscn  11036  axpre-sup  11057  1re  11109  0re  11111  00id  11285  addrid  11290  0cnALT  11345  renegcli  11419  zexALT  12485  uzn0  12746  xrinfmss  13206  axdc4uzlem  13887  facnn  14179  fac0  14180  hashgval  14237  hashinf  14239  hashresfn  14244  hashrabrsn  14276  hashrabsn01  14277  hashrabsn1  14278  hashp1i  14307  hash1snb  14323  hashxplem  14337  fi1uzind  14411  cshw1  14726  cats1fv  14763  s7f1o  14870  trclubgi  14901  cnrecnv  15069  rexanuz  15250  climdm  15458  lo1eq  15472  rlimeq  15473  sumsnf  15647  tanval  16034  rpnnen2lem11  16130  rpnnen  16133  sadadd2lem  16367  sadadd3  16369  sadaddlem  16374  sadasslem  16378  sadeq  16380  lcmgcdlem  16514  unbenlem  16817  prmreclem6  16830  vdwlem8  16897  vdwnnlem1  16904  0ram  16929  structcnvcnv  17061  prdsvallem  17355  prdsval  17356  prdsbas  17358  prdsplusg  17359  prdsmulr  17360  prdsvsca  17361  prdshom  17368  xpsfrn  17469  xpsff1o2  17470  catcoppccl  18021  catcfuccl  18022  catcxpccl  18110  tsrss  18492  gsumpropd2lem  18584  smndex2dnrinv  18820  mvdco  19355  efgmnvl  19624  efgval  19627  efgi0  19630  efgi1  19631  efgredeu  19662  0frgp  19689  abln0  19777  lt6abl  19805  gsumval3  19817  gsum2dlem2  19881  dprdres  19940  dmdprdsplit2lem  19957  ringn0  20227  isdrng2  20656  drngmclOLD  20664  drngid2  20665  cnfldplusf  21331  cnfldsub  21332  cnsubmlem  21349  cnsubglem  21350  cnmsubglem  21365  gzrngunitlem  21367  rge0srg  21373  zring0  21393  pzriprnglem10  21425  zzngim  21487  zrhpsgnmhm  21519  re0g  21547  pjfval  21641  pjpm  21643  psrplusg  21871  coe1sfi  22124  ply1plusgfvi  22152  marep01ma  22573  smadiadetlem1a  22576  smadiadetlem3lem2  22580  smadiadetlem3  22581  smadiadetlem4  22582  smadiadet  22583  indistpsALT  22926  tgrest  23072  leordtval2  23125  lmbr2  23172  cnprest  23202  lmff  23214  kgenidm  23460  tx1cn  23522  tx2cn  23523  ustbas  24140  psmetge0  24225  xmetge0  24257  qdensere  24682  cnblcld  24687  cnfldms  24688  cnfldtopn  24694  xrsdsre  24724  xrge0tsms  24748  iccpnfcnv  24867  xrhmeo  24869  cnheiborlem  24878  cnlmod  25065  recvs  25071  lmmbr2  25184  lmcau  25238  metsscmetcld  25240  cncms  25280  cnfldcusp  25282  ovolctb  25416  ovoliunnul  25433  ismbl  25452  volf  25455  voliunlem1  25476  ioorf  25499  ioorinv  25502  ioorcl  25503  dyaddisj  25522  dyadmax  25524  dyadmbl  25526  mbfid  25561  ismbfd  25565  mbfimaopnlem  25581  limcresi  25811  dvreslem  25835  dvres2lem  25836  dvcjbr  25878  dvferm1  25914  dvferm2  25916  dvlip2  25925  dv11cn  25931  deg1ldg  26022  deg1leb  26025  plycpn  26222  vieta1lem2  26244  elqaa  26255  aalioulem2  26266  aaliou3lem3  26277  aaliou3lem4  26279  pserulm  26356  psercnlem2  26359  psercnlem1  26360  psercn  26361  abelth  26376  reeff1o  26382  pilem1  26386  efhalfpi  26405  coseq0negpitopi  26437  pige3ALT  26454  tanregt0  26473  efif1olem3  26478  efif1olem4  26479  efifo  26481  eff1olem  26482  efsubm  26485  logrn  26492  ellogrn  26493  relogf1o  26500  argregt0  26544  argrege0  26545  dvrelog  26571  dvloglem  26582  logf1o2  26584  dvlog  26585  efopnlem1  26590  efopnlem2  26591  logtayl  26594  cxpcn3lem  26682  cxpcn3  26683  resqrtcn  26684  asinneg  26821  asinrebnd  26836  atan0  26843  atanbnd  26861  areambl  26893  sqrtlim  26908  amgmlem  26925  lgamucov  26973  basellem1  27016  basellem4  27019  sqff1o  27117  dchrplusg  27183  bposlem6  27225  bposlem8  27227  dchrvmasumlem2  27434  pntibndlem1  27525  pntlemo  27543  qrng0  27557  ostth  27575  noextendseq  27604  bday0s  27770  oldlim  27830  zsex  28302  lmif  28761  islmib  28763  structiedg0val  28998  snstriedgval  29014  umgredgnlp  29123  usgrexmplef  29235  usgrexmpledg  29238  vtxdlfgrval  29462  upgr2pthnlp  29708  konigsberglem5  30231  ex-mod  30424  pliguhgr  30461  grporn  30496  ip0i  30800  ubthlem1  30845  ubthlem2  30846  axhcompl-zf  30973  normlem7  31091  bcseqi  31095  bcsiALT  31154  hlimf  31212  hlimuni  31213  hhssabloilem  31236  hhshsslem1  31242  hhsssh  31244  hhsscms  31253  occllem  31278  occl  31279  h1deoi  31524  h1dei  31525  h1de2ctlem  31530  h1de2ci  31531  spansni  31532  spanunsni  31554  pjpythi  31697  nmfn0  31962  nmopadjlem  32064  adjcoi  32075  nmopcoadji  32076  pjoccoi  32153  shatomistici  32336  iuninc  32535  imadifxp  32576  xppreima  32622  1stpreima  32683  2ndpreima  32684  fsuppcurry1  32702  fsuppcurry2  32703  hashgt1  32785  s3clhash  32924  gsummpt2d  33024  xrge0tsmsd  33037  tocyc01  33082  cyc3evpm  33114  cycpmconjslem2  33119  cyc3conja  33121  reofld  33303  rearchi  33306  nn0archi  33307  xrge0slmod  33308  elrspunidl  33388  dimval  33608  dimvalfi  33609  ply1degltdimlem  33630  algextdeglem8  33732  qtophaus  33844  iistmd  33910  xpinpreima  33914  xpinpreima2  33915  tpr2rico  33920  mndpluscn  33934  xrge0pluscn  33948  cnzh  33976  rezh  33977  qqhucn  34000  rrhcn  34005  cnrrext  34018  zrhre  34027  qqhre  34028  ismntop  34034  sigaex  34118  brsiga  34191  cntnevol  34236  voliune  34237  ddemeas  34244  1stmbfm  34268  2ndmbfm  34269  br2base  34277  dya2icoseg2  34286  dya2iocucvr  34292  carsgclctunlem2  34327  carsgclctunlem3  34328  sitgaddlemb  34356  eulerpartlemt  34379  eulerpartgbij  34380  eulerpartlemmf  34383  eulerpartlemgvv  34384  eulerpartlemgf  34387  eulerpart  34390  sseqmw  34399  sseqf  34400  sseqp1  34403  fiblem  34406  fibp1  34409  dstrvprob  34480  coinflipspace  34489  coinfliprv  34491  coinflippv  34492  ballotlem1  34495  ballotlem8  34545  circlemethhgt  34651  onvf1od  35139  usgrcyclgt2v  35163  iccllysconn  35282  rellysconn  35283  satf00  35406  fmla0  35414  msrid  35577  dfrdg2  35828  dfrdg4  35984  imagesset  35986  elhf  36207  filnetlem3  36413  limsucncmpi  36478  bj-babygodel  36636  bj-idres  37193  taupilem3  37352  icoreresf  37385  icoreelrnab  37387  relowlssretop  37396  poimirlem3  37662  poimirlem9  37668  poimirlem15  37674  poimirlem16  37675  poimirlem17  37676  poimirlem19  37678  poimirlem27  37686  poimirlem28  37687  poimirlem31  37690  poimirlem32  37691  mblfinlem1  37696  ovoliunnfl  37701  voliunnfl  37703  mbfresfi  37705  dvtan  37709  itg2addnc  37713  ftc1anclem3  37734  areacirc  37752  fdc  37784  ismrer1  37877  reheibor  37878  rngomndo  37974  gidsn  37991  ac6s6f  38212  cnvref4  38377  dfcnvrefrels2  38564  dfcnvrefrels3  38565  dedths  39000  tendo0co2  40826  erng1r  41033  dvalveclem  41063  dva0g  41065  dvh0g  41149  sn-it0e0  42448  sn-0tie0  42483  2rexfrabdioph  42828  3rexfrabdioph  42829  4rexfrabdioph  42830  6rexfrabdioph  42831  7rexfrabdioph  42832  rencldnfi  42853  jm2.27dlem2  43042  wepwso  43075  dfac11  43094  pwssplit4  43121  frlmpwfi  43130  isnumbasgrplem3  43137  mpaaeu  43182  proot1mul  43226  proot1hash  43227  epirron  43286  oneptr  43287  ordeldif1o  43292  oaomoencom  43349  oenassex  43350  cnvcnvintabd  43632  cnvrcl0  43657  dfrtrcl5  43661  cotrcltrcl  43757  frege92  43987  seff  44341  prmunb2  44343  binomcxplemdvbinom  44385  binomcxplemcvg  44386  binomcxplemnotnn0  44388  permac8prim  45046  sumsnd  45062  islptre  45658  stoweidlem34  46071  stoweidlem37  46074  stirlinglem11  46121  stirlinglem12  46122  stirlinglem13  46123  fouriersw  46268  natlocalincr  46913  fundcmpsurbijinjpreimafv  47437  fundcmpsurinjimaid  47441  fmtnoinf  47566  gbowge7  47793  nnsum3primes4  47818  usgrexmpl12ngrlic  48069  gpgprismgr4cycllem2  48126  gpg5ngric  48158  2zrng0  48274  lmodn0  48526  zlmodzxzldeplem3  48533  lvecpsslmod  48538  0dig2pr01  48641  nelsubc3lem  49101  aacllem  49832  amgmwlem  49833