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  ceqsexv2dOLD  3480  dtruALT2  5312  intasym  6078  relcoi2  6241  funres11  6575  cnvresid  6577  find  7846  fparlem1  8062  fparlem2  8063  dftpos4  8195  tposf12  8201  tfr2b  8335  tz7.44lem1  8344  ord3  8420  xp01disjl  8427  on2recsfn  8603  on2recsov  8604  on2ind  8605  on3ind  8606  xpcomco  9005  sbthlem2  9026  fidomdm  9244  brwdom2  9488  epnsym  9530  inf3lem6  9554  cnfcom  9621  ttrclco  9639  ttrclselem2  9647  tz9.1c  9651  frr1  9683  r1tr  9700  r1ord3g  9703  rankwflemb  9717  r1elwf  9720  r1elss  9730  rankval3b  9750  onssr1  9755  inlresf  9838  inrresf  9840  djuin  9842  infxpenlem  9935  alephnbtwn  9993  alephordilem1  9995  alephfp  10030  dfac13  10065  pwsdompw  10125  infdjuabs  10127  ackbij1  10159  ackbij2  10164  r1om  10165  cflim2  10185  fin23lem27  10250  fin23lem29  10263  fin23lem30  10264  fin1a2lem6  10327  fin1a2lem7  10328  fin1a2lem13  10334  itunitc1  10342  itunitc  10343  ituniiun  10344  hsmexlem5  10352  axcc2lem  10358  axcc3  10360  zorn2lem6  10423  zorn2lem7  10424  ttukeylem6  10436  dmct  10446  iunfo  10461  cardval  10468  cardid  10469  alephom  10508  canthp1lem2  10576  gchaleph2  10595  r1limwun  10659  inaprc  10759  nqerf  10853  recmulnq  10887  dmrecnq  10891  halfnq  10899  genpdm  10925  reclem3pr  10972  axresscn  11071  axpre-sup  11092  1re  11144  0re  11146  00id  11321  addrid  11326  0cnALT  11381  renegcli  11455  zexALT  12544  uzn0  12805  xrinfmss  13262  axdc4uzlem  13945  facnn  14237  fac0  14238  hashgval  14295  hashinf  14297  hashresfn  14302  hashrabrsn  14334  hashrabsn01  14335  hashrabsn1  14336  hashp1i  14365  hash1snb  14381  hashxplem  14395  fi1uzind  14469  cshw1  14784  cats1fv  14821  s7f1o  14928  trclubgi  14959  cnrecnv  15127  rexanuz  15308  climdm  15516  lo1eq  15530  rlimeq  15531  sumsnf  15705  tanval  16095  rpnnen2lem11  16191  rpnnen  16194  sadadd2lem  16428  sadadd3  16430  sadaddlem  16435  sadasslem  16439  sadeq  16441  lcmgcdlem  16575  unbenlem  16879  prmreclem6  16892  vdwlem8  16959  vdwnnlem1  16966  0ram  16991  structcnvcnv  17123  prdsvallem  17417  prdsval  17418  prdsbas  17420  prdsplusg  17421  prdsmulr  17422  prdsvsca  17423  prdshom  17430  xpsfrn  17532  xpsff1o2  17533  catcoppccl  18084  catcfuccl  18085  catcxpccl  18173  tsrss  18555  gsumpropd2lem  18647  smndex2dnrinv  18886  mvdco  19420  efgmnvl  19689  efgval  19692  efgi0  19695  efgi1  19696  efgredeu  19727  0frgp  19754  abln0  19842  lt6abl  19870  gsumval3  19882  gsum2dlem2  19946  dprdres  20005  dmdprdsplit2lem  20022  ringn0  20292  isdrng2  20720  drngmclOLD  20728  drngid2  20729  cnfldplusf  21379  cnfldsub  21380  cnsubmlem  21395  cnsubglem  21396  cnmsubglem  21410  gzrngunitlem  21412  rge0srg  21418  zring0  21438  pzriprnglem10  21470  zzngim  21532  zrhpsgnmhm  21564  re0g  21592  pjfval  21686  pjpm  21688  psrplusg  21916  coe1sfi  22177  ply1plusgfvi  22205  marep01ma  22625  smadiadetlem1a  22628  smadiadetlem3lem2  22632  smadiadetlem3  22633  smadiadetlem4  22634  smadiadet  22635  indistpsALT  22978  tgrest  23124  leordtval2  23177  lmbr2  23224  cnprest  23254  lmff  23266  kgenidm  23512  tx1cn  23574  tx2cn  23575  ustbas  24192  psmetge0  24277  xmetge0  24309  qdensere  24734  cnblcld  24739  cnfldms  24740  cnfldtopn  24746  xrsdsre  24776  xrge0tsms  24800  iccpnfcnv  24911  xrhmeo  24913  cnheiborlem  24921  cnlmod  25107  recvs  25113  lmmbr2  25226  lmcau  25280  metsscmetcld  25282  cncms  25322  cnfldcusp  25324  ovolctb  25457  ovoliunnul  25474  ismbl  25493  volf  25496  voliunlem1  25517  ioorf  25540  ioorinv  25543  ioorcl  25544  dyaddisj  25563  dyadmax  25565  dyadmbl  25567  mbfid  25602  ismbfd  25606  mbfimaopnlem  25622  limcresi  25852  dvreslem  25876  dvres2lem  25877  dvcjbr  25916  dvferm1  25952  dvferm2  25954  dvlip2  25962  dv11cn  25968  deg1ldg  26057  deg1leb  26060  plycpn  26255  vieta1lem2  26277  elqaa  26288  aalioulem2  26299  aaliou3lem3  26310  aaliou3lem4  26312  pserulm  26387  psercnlem2  26389  psercnlem1  26390  psercn  26391  abelth  26406  reeff1o  26412  pilem1  26416  efhalfpi  26435  coseq0negpitopi  26467  pige3ALT  26484  tanregt0  26503  efif1olem3  26508  efif1olem4  26509  efifo  26511  eff1olem  26512  efsubm  26515  logrn  26522  ellogrn  26523  relogf1o  26530  argregt0  26574  argrege0  26575  dvrelog  26601  dvloglem  26612  logf1o2  26614  dvlog  26615  efopnlem1  26620  efopnlem2  26621  logtayl  26624  cxpcn3lem  26711  cxpcn3  26712  resqrtcn  26713  asinneg  26850  asinrebnd  26865  atan0  26872  atanbnd  26890  areambl  26922  sqrtlim  26936  amgmlem  26953  lgamucov  27001  basellem1  27044  basellem4  27047  sqff1o  27145  dchrplusg  27210  bposlem6  27252  bposlem8  27254  dchrvmasumlem2  27461  pntibndlem1  27552  pntlemo  27570  qrng0  27584  ostth  27602  noextendseq  27631  bday0  27803  oldlim  27879  ons2ind  28267  zsex  28372  lmif  28853  islmib  28855  structiedg0val  29091  snstriedgval  29107  umgredgnlp  29216  usgrexmplef  29328  usgrexmpledg  29331  vtxdlfgrval  29554  upgr2pthnlp  29800  konigsberglem5  30326  ex-mod  30519  nowisdomv  30544  pliguhgr  30557  grporn  30592  ip0i  30896  ubthlem1  30941  ubthlem2  30942  axhcompl-zf  31069  normlem7  31187  bcseqi  31191  bcsiALT  31250  hlimf  31308  hlimuni  31309  hhssabloilem  31332  hhshsslem1  31338  hhsssh  31340  hhsscms  31349  occllem  31374  occl  31375  h1deoi  31620  h1dei  31621  h1de2ctlem  31626  h1de2ci  31627  spansni  31628  spanunsni  31650  pjpythi  31793  nmfn0  32058  nmopadjlem  32160  adjcoi  32171  nmopcoadji  32172  pjoccoi  32249  shatomistici  32432  iuninc  32630  imadifxp  32671  xppreima  32718  1stpreima  32780  2ndpreima  32781  fsuppcurry1  32797  fsuppcurry2  32798  hashgt1  32881  s3clhash  33008  gsummpt2d  33110  xrge0tsmsd  33134  tocyc01  33179  cyc3evpm  33211  cycpmconjslem2  33216  cyc3conja  33218  reofld  33403  rearchi  33406  nn0archi  33407  xrge0slmod  33408  elrspunidl  33488  dimval  33745  dimvalfi  33746  ply1degltdimlem  33766  algextdeglem8  33868  qtophaus  33980  iistmd  34046  xpinpreima  34050  xpinpreima2  34051  tpr2rico  34056  mndpluscn  34070  xrge0pluscn  34084  cnzh  34112  rezh  34113  qqhucn  34136  rrhcn  34141  cnrrext  34154  zrhre  34163  qqhre  34164  ismntop  34170  sigaex  34254  brsiga  34327  cntnevol  34372  voliune  34373  ddemeas  34380  1stmbfm  34404  2ndmbfm  34405  br2base  34413  dya2icoseg2  34422  dya2iocucvr  34428  carsgclctunlem2  34463  carsgclctunlem3  34464  sitgaddlemb  34492  eulerpartlemt  34515  eulerpartgbij  34516  eulerpartlemmf  34519  eulerpartlemgvv  34520  eulerpartlemgf  34523  eulerpart  34526  sseqmw  34535  sseqf  34536  sseqp1  34539  fiblem  34542  fibp1  34545  dstrvprob  34616  coinflipspace  34625  coinfliprv  34627  coinflippv  34628  ballotlem1  34631  ballotlem8  34681  circlemethhgt  34787  r11  35237  r12  35238  onvf1od  35289  usgrcyclgt2v  35313  iccllysconn  35432  rellysconn  35433  satf00  35556  fmla0  35564  msrid  35727  dfrdg2  35975  dfrdg4  36133  imagesset  36135  elhf  36356  filnetlem3  36562  limsucncmpi  36627  ttciunun  36693  bj-babygodel  36868  bj-idres  37474  taupilem3  37633  icoreresf  37668  icoreelrnab  37670  relowlssretop  37679  poimirlem3  37944  poimirlem9  37950  poimirlem15  37956  poimirlem16  37957  poimirlem17  37958  poimirlem19  37960  poimirlem27  37968  poimirlem28  37969  poimirlem31  37972  poimirlem32  37973  mblfinlem1  37978  ovoliunnfl  37983  voliunnfl  37985  mbfresfi  37987  dvtan  37991  itg2addnc  37995  ftc1anclem3  38016  areacirc  38034  fdc  38066  ismrer1  38159  reheibor  38160  rngomndo  38256  gidsn  38273  ac6s6f  38494  cnvref4  38671  dfcnvrefrels2  38929  dfcnvrefrels3  38930  dedths  39408  tendo0co2  41234  erng1r  41441  dvalveclem  41471  dva0g  41473  dvh0g  41557  sn-it0e0  42848  sn-0tie0  42896  2rexfrabdioph  43224  3rexfrabdioph  43225  4rexfrabdioph  43226  6rexfrabdioph  43227  7rexfrabdioph  43228  rencldnfi  43249  jm2.27dlem2  43438  wepwso  43471  dfac11  43490  pwssplit4  43517  frlmpwfi  43526  isnumbasgrplem3  43533  mpaaeu  43578  proot1mul  43622  proot1hash  43623  epirron  43682  oneptr  43683  ordeldif1o  43688  oaomoencom  43745  oenassex  43746  cnvcnvintabd  44027  cnvrcl0  44052  dfrtrcl5  44056  cotrcltrcl  44152  frege92  44382  seff  44736  prmunb2  44738  binomcxplemdvbinom  44780  binomcxplemcvg  44781  binomcxplemnotnn0  44783  permac8prim  45441  sumsnd  45457  islptre  46049  stoweidlem34  46462  stoweidlem37  46465  stirlinglem11  46512  stirlinglem12  46513  stirlinglem13  46514  fouriersw  46659  natlocalincr  47306  nthrucw  47316  fundcmpsurbijinjpreimafv  47867  fundcmpsurinjimaid  47871  fmtnoinf  47999  gbowge7  48239  nnsum3primes4  48264  usgrexmpl12ngrlic  48515  gpgprismgr4cycllem2  48572  gpg5ngric  48604  2zrng0  48720  lmodn0  48971  zlmodzxzldeplem3  48978  lvecpsslmod  48983  0dig2pr01  49086  nelsubc3lem  49545  aacllem  50276  amgmwlem  50277