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  5310  intasym  6066  relcoi2  6229  funres11  6563  cnvresid  6565  find  7831  fparlem1  8048  fparlem2  8049  dftpos4  8181  tposf12  8187  tfr2b  8321  tz7.44lem1  8330  ord3  8406  xp01disjl  8413  on2recsfn  8588  on2recsov  8589  on2ind  8590  on3ind  8591  xpcomco  8987  sbthlem2  9008  fidomdm  9225  brwdom2  9466  epnsym  9506  inf3lem6  9530  cnfcom  9597  ttrclco  9615  ttrclselem2  9623  tz9.1c  9627  frr1  9659  r1tr  9676  r1ord3g  9679  rankwflemb  9693  r1elwf  9696  r1elss  9706  rankval3b  9726  onssr1  9731  inlresf  9814  inrresf  9816  djuin  9818  infxpenlem  9911  alephnbtwn  9969  alephordilem1  9971  alephfp  10006  dfac13  10041  pwsdompw  10101  infdjuabs  10103  ackbij1  10135  ackbij2  10140  r1om  10141  cflim2  10161  fin23lem27  10226  fin23lem29  10239  fin23lem30  10240  fin1a2lem6  10303  fin1a2lem7  10304  fin1a2lem13  10310  itunitc1  10318  itunitc  10319  ituniiun  10320  hsmexlem5  10328  axcc2lem  10334  axcc3  10336  zorn2lem6  10399  zorn2lem7  10400  ttukeylem6  10412  dmct  10422  iunfo  10437  cardval  10444  cardid  10445  alephom  10483  canthp1lem2  10551  gchaleph2  10570  r1limwun  10634  inaprc  10734  nqerf  10828  recmulnq  10862  dmrecnq  10866  halfnq  10874  genpdm  10900  reclem3pr  10947  axresscn  11046  axpre-sup  11067  1re  11119  0re  11121  00id  11295  addrid  11300  0cnALT  11355  renegcli  11429  zexALT  12495  uzn0  12755  xrinfmss  13211  axdc4uzlem  13892  facnn  14184  fac0  14185  hashgval  14242  hashinf  14244  hashresfn  14249  hashrabrsn  14281  hashrabsn01  14282  hashrabsn1  14283  hashp1i  14312  hash1snb  14328  hashxplem  14342  fi1uzind  14416  cshw1  14731  cats1fv  14768  s7f1o  14875  trclubgi  14906  cnrecnv  15074  rexanuz  15255  climdm  15463  lo1eq  15477  rlimeq  15478  sumsnf  15652  tanval  16039  rpnnen2lem11  16135  rpnnen  16138  sadadd2lem  16372  sadadd3  16374  sadaddlem  16379  sadasslem  16383  sadeq  16385  lcmgcdlem  16519  unbenlem  16822  prmreclem6  16835  vdwlem8  16902  vdwnnlem1  16909  0ram  16934  structcnvcnv  17066  prdsvallem  17360  prdsval  17361  prdsbas  17363  prdsplusg  17364  prdsmulr  17365  prdsvsca  17366  prdshom  17373  xpsfrn  17474  xpsff1o2  17475  catcoppccl  18026  catcfuccl  18027  catcxpccl  18115  tsrss  18497  gsumpropd2lem  18589  smndex2dnrinv  18825  mvdco  19359  efgmnvl  19628  efgval  19631  efgi0  19634  efgi1  19635  efgredeu  19666  0frgp  19693  abln0  19781  lt6abl  19809  gsumval3  19821  gsum2dlem2  19885  dprdres  19944  dmdprdsplit2lem  19961  ringn0  20231  isdrng2  20660  drngmclOLD  20668  drngid2  20669  cnfldplusf  21335  cnfldsub  21336  cnsubmlem  21353  cnsubglem  21354  cnmsubglem  21369  gzrngunitlem  21371  rge0srg  21377  zring0  21397  pzriprnglem10  21429  zzngim  21491  zrhpsgnmhm  21523  re0g  21551  pjfval  21645  pjpm  21647  psrplusg  21875  coe1sfi  22127  ply1plusgfvi  22155  marep01ma  22576  smadiadetlem1a  22579  smadiadetlem3lem2  22583  smadiadetlem3  22584  smadiadetlem4  22585  smadiadet  22586  indistpsALT  22929  tgrest  23075  leordtval2  23128  lmbr2  23175  cnprest  23205  lmff  23217  kgenidm  23463  tx1cn  23525  tx2cn  23526  ustbas  24143  psmetge0  24228  xmetge0  24260  qdensere  24685  cnblcld  24690  cnfldms  24691  cnfldtopn  24697  xrsdsre  24727  xrge0tsms  24751  iccpnfcnv  24870  xrhmeo  24872  cnheiborlem  24881  cnlmod  25068  recvs  25074  lmmbr2  25187  lmcau  25241  metsscmetcld  25243  cncms  25283  cnfldcusp  25285  ovolctb  25419  ovoliunnul  25436  ismbl  25455  volf  25458  voliunlem1  25479  ioorf  25502  ioorinv  25505  ioorcl  25506  dyaddisj  25525  dyadmax  25527  dyadmbl  25529  mbfid  25564  ismbfd  25568  mbfimaopnlem  25584  limcresi  25814  dvreslem  25838  dvres2lem  25839  dvcjbr  25881  dvferm1  25917  dvferm2  25919  dvlip2  25928  dv11cn  25934  deg1ldg  26025  deg1leb  26028  plycpn  26225  vieta1lem2  26247  elqaa  26258  aalioulem2  26269  aaliou3lem3  26280  aaliou3lem4  26282  pserulm  26359  psercnlem2  26362  psercnlem1  26363  psercn  26364  abelth  26379  reeff1o  26385  pilem1  26389  efhalfpi  26408  coseq0negpitopi  26440  pige3ALT  26457  tanregt0  26476  efif1olem3  26481  efif1olem4  26482  efifo  26484  eff1olem  26485  efsubm  26488  logrn  26495  ellogrn  26496  relogf1o  26503  argregt0  26547  argrege0  26548  dvrelog  26574  dvloglem  26585  logf1o2  26587  dvlog  26588  efopnlem1  26593  efopnlem2  26594  logtayl  26597  cxpcn3lem  26685  cxpcn3  26686  resqrtcn  26687  asinneg  26824  asinrebnd  26839  atan0  26846  atanbnd  26864  areambl  26896  sqrtlim  26911  amgmlem  26928  lgamucov  26976  basellem1  27019  basellem4  27022  sqff1o  27120  dchrplusg  27186  bposlem6  27228  bposlem8  27230  dchrvmasumlem2  27437  pntibndlem1  27528  pntlemo  27546  qrng0  27560  ostth  27578  noextendseq  27607  bday0s  27773  oldlim  27833  zsex  28305  lmif  28764  islmib  28766  structiedg0val  29002  snstriedgval  29018  umgredgnlp  29127  usgrexmplef  29239  usgrexmpledg  29242  vtxdlfgrval  29466  upgr2pthnlp  29712  konigsberglem5  30238  ex-mod  30431  pliguhgr  30468  grporn  30503  ip0i  30807  ubthlem1  30852  ubthlem2  30853  axhcompl-zf  30980  normlem7  31098  bcseqi  31102  bcsiALT  31161  hlimf  31219  hlimuni  31220  hhssabloilem  31243  hhshsslem1  31249  hhsssh  31251  hhsscms  31260  occllem  31285  occl  31286  h1deoi  31531  h1dei  31532  h1de2ctlem  31537  h1de2ci  31538  spansni  31539  spanunsni  31561  pjpythi  31704  nmfn0  31969  nmopadjlem  32071  adjcoi  32082  nmopcoadji  32083  pjoccoi  32160  shatomistici  32343  iuninc  32542  imadifxp  32583  xppreima  32629  1stpreima  32692  2ndpreima  32693  fsuppcurry1  32711  fsuppcurry2  32712  hashgt1  32795  s3clhash  32936  gsummpt2d  33036  xrge0tsmsd  33049  tocyc01  33094  cyc3evpm  33126  cycpmconjslem2  33131  cyc3conja  33133  reofld  33315  rearchi  33318  nn0archi  33319  xrge0slmod  33320  elrspunidl  33400  dimval  33634  dimvalfi  33635  ply1degltdimlem  33656  algextdeglem8  33758  qtophaus  33870  iistmd  33936  xpinpreima  33940  xpinpreima2  33941  tpr2rico  33946  mndpluscn  33960  xrge0pluscn  33974  cnzh  34002  rezh  34003  qqhucn  34026  rrhcn  34031  cnrrext  34044  zrhre  34053  qqhre  34054  ismntop  34060  sigaex  34144  brsiga  34217  cntnevol  34262  voliune  34263  ddemeas  34270  1stmbfm  34294  2ndmbfm  34295  br2base  34303  dya2icoseg2  34312  dya2iocucvr  34318  carsgclctunlem2  34353  carsgclctunlem3  34354  sitgaddlemb  34382  eulerpartlemt  34405  eulerpartgbij  34406  eulerpartlemmf  34409  eulerpartlemgvv  34410  eulerpartlemgf  34413  eulerpart  34416  sseqmw  34425  sseqf  34426  sseqp1  34429  fiblem  34432  fibp1  34435  dstrvprob  34506  coinflipspace  34515  coinfliprv  34517  coinflippv  34518  ballotlem1  34521  ballotlem8  34571  circlemethhgt  34677  r11  35126  r12  35127  onvf1od  35172  usgrcyclgt2v  35196  iccllysconn  35315  rellysconn  35316  satf00  35439  fmla0  35447  msrid  35610  dfrdg2  35858  dfrdg4  36016  imagesset  36018  elhf  36239  filnetlem3  36445  limsucncmpi  36510  bj-babygodel  36668  bj-idres  37225  taupilem3  37384  icoreresf  37417  icoreelrnab  37419  relowlssretop  37428  poimirlem3  37683  poimirlem9  37689  poimirlem15  37695  poimirlem16  37696  poimirlem17  37697  poimirlem19  37699  poimirlem27  37707  poimirlem28  37708  poimirlem31  37711  poimirlem32  37712  mblfinlem1  37717  ovoliunnfl  37722  voliunnfl  37724  mbfresfi  37726  dvtan  37730  itg2addnc  37734  ftc1anclem3  37755  areacirc  37773  fdc  37805  ismrer1  37898  reheibor  37899  rngomndo  37995  gidsn  38012  ac6s6f  38233  cnvref4  38402  dfcnvrefrels2  38640  dfcnvrefrels3  38641  dedths  39081  tendo0co2  40907  erng1r  41114  dvalveclem  41144  dva0g  41146  dvh0g  41230  sn-it0e0  42534  sn-0tie0  42569  2rexfrabdioph  42913  3rexfrabdioph  42914  4rexfrabdioph  42915  6rexfrabdioph  42916  7rexfrabdioph  42917  rencldnfi  42938  jm2.27dlem2  43127  wepwso  43160  dfac11  43179  pwssplit4  43206  frlmpwfi  43215  isnumbasgrplem3  43222  mpaaeu  43267  proot1mul  43311  proot1hash  43312  epirron  43371  oneptr  43372  ordeldif1o  43377  oaomoencom  43434  oenassex  43435  cnvcnvintabd  43717  cnvrcl0  43742  dfrtrcl5  43746  cotrcltrcl  43842  frege92  44072  seff  44426  prmunb2  44428  binomcxplemdvbinom  44470  binomcxplemcvg  44471  binomcxplemnotnn0  44473  permac8prim  45131  sumsnd  45147  islptre  45743  stoweidlem34  46156  stoweidlem37  46159  stirlinglem11  46206  stirlinglem12  46207  stirlinglem13  46208  fouriersw  46353  natlocalincr  46998  nthrucw  47008  fundcmpsurbijinjpreimafv  47531  fundcmpsurinjimaid  47535  fmtnoinf  47660  gbowge7  47887  nnsum3primes4  47912  usgrexmpl12ngrlic  48163  gpgprismgr4cycllem2  48220  gpg5ngric  48252  2zrng0  48368  lmodn0  48620  zlmodzxzldeplem3  48627  lvecpsslmod  48632  0dig2pr01  48735  nelsubc3lem  49195  aacllem  49926  amgmwlem  49927