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  3492  dtruALT2  5315  intasym  6072  relcoi2  6235  funres11  6569  cnvresid  6571  find  7837  fparlem1  8054  fparlem2  8055  dftpos4  8187  tposf12  8193  tfr2b  8327  tz7.44lem1  8336  ord3  8412  xp01disjl  8419  on2recsfn  8595  on2recsov  8596  on2ind  8597  on3ind  8598  xpcomco  8995  sbthlem2  9016  fidomdm  9234  brwdom2  9478  epnsym  9518  inf3lem6  9542  cnfcom  9609  ttrclco  9627  ttrclselem2  9635  tz9.1c  9639  frr1  9671  r1tr  9688  r1ord3g  9691  rankwflemb  9705  r1elwf  9708  r1elss  9718  rankval3b  9738  onssr1  9743  inlresf  9826  inrresf  9828  djuin  9830  infxpenlem  9923  alephnbtwn  9981  alephordilem1  9983  alephfp  10018  dfac13  10053  pwsdompw  10113  infdjuabs  10115  ackbij1  10147  ackbij2  10152  r1om  10153  cflim2  10173  fin23lem27  10238  fin23lem29  10251  fin23lem30  10252  fin1a2lem6  10315  fin1a2lem7  10316  fin1a2lem13  10322  itunitc1  10330  itunitc  10331  ituniiun  10332  hsmexlem5  10340  axcc2lem  10346  axcc3  10348  zorn2lem6  10411  zorn2lem7  10412  ttukeylem6  10424  dmct  10434  iunfo  10449  cardval  10456  cardid  10457  alephom  10496  canthp1lem2  10564  gchaleph2  10583  r1limwun  10647  inaprc  10747  nqerf  10841  recmulnq  10875  dmrecnq  10879  halfnq  10887  genpdm  10913  reclem3pr  10960  axresscn  11059  axpre-sup  11080  1re  11132  0re  11134  00id  11308  addrid  11313  0cnALT  11368  renegcli  11442  zexALT  12508  uzn0  12768  xrinfmss  13225  axdc4uzlem  13906  facnn  14198  fac0  14199  hashgval  14256  hashinf  14258  hashresfn  14263  hashrabrsn  14295  hashrabsn01  14296  hashrabsn1  14297  hashp1i  14326  hash1snb  14342  hashxplem  14356  fi1uzind  14430  cshw1  14745  cats1fv  14782  s7f1o  14889  trclubgi  14920  cnrecnv  15088  rexanuz  15269  climdm  15477  lo1eq  15491  rlimeq  15492  sumsnf  15666  tanval  16053  rpnnen2lem11  16149  rpnnen  16152  sadadd2lem  16386  sadadd3  16388  sadaddlem  16393  sadasslem  16397  sadeq  16399  lcmgcdlem  16533  unbenlem  16836  prmreclem6  16849  vdwlem8  16916  vdwnnlem1  16923  0ram  16948  structcnvcnv  17080  prdsvallem  17374  prdsval  17375  prdsbas  17377  prdsplusg  17378  prdsmulr  17379  prdsvsca  17380  prdshom  17387  xpsfrn  17489  xpsff1o2  17490  catcoppccl  18041  catcfuccl  18042  catcxpccl  18130  tsrss  18512  gsumpropd2lem  18604  smndex2dnrinv  18840  mvdco  19374  efgmnvl  19643  efgval  19646  efgi0  19649  efgi1  19650  efgredeu  19681  0frgp  19708  abln0  19796  lt6abl  19824  gsumval3  19836  gsum2dlem2  19900  dprdres  19959  dmdprdsplit2lem  19976  ringn0  20246  isdrng2  20676  drngmclOLD  20684  drngid2  20685  cnfldplusf  21351  cnfldsub  21352  cnsubmlem  21369  cnsubglem  21370  cnmsubglem  21385  gzrngunitlem  21387  rge0srg  21393  zring0  21413  pzriprnglem10  21445  zzngim  21507  zrhpsgnmhm  21539  re0g  21567  pjfval  21661  pjpm  21663  psrplusg  21892  coe1sfi  22154  ply1plusgfvi  22182  marep01ma  22604  smadiadetlem1a  22607  smadiadetlem3lem2  22611  smadiadetlem3  22612  smadiadetlem4  22613  smadiadet  22614  indistpsALT  22957  tgrest  23103  leordtval2  23156  lmbr2  23203  cnprest  23233  lmff  23245  kgenidm  23491  tx1cn  23553  tx2cn  23554  ustbas  24171  psmetge0  24256  xmetge0  24288  qdensere  24713  cnblcld  24718  cnfldms  24719  cnfldtopn  24725  xrsdsre  24755  xrge0tsms  24779  iccpnfcnv  24898  xrhmeo  24900  cnheiborlem  24909  cnlmod  25096  recvs  25102  lmmbr2  25215  lmcau  25269  metsscmetcld  25271  cncms  25311  cnfldcusp  25313  ovolctb  25447  ovoliunnul  25464  ismbl  25483  volf  25486  voliunlem1  25507  ioorf  25530  ioorinv  25533  ioorcl  25534  dyaddisj  25553  dyadmax  25555  dyadmbl  25557  mbfid  25592  ismbfd  25596  mbfimaopnlem  25612  limcresi  25842  dvreslem  25866  dvres2lem  25867  dvcjbr  25909  dvferm1  25945  dvferm2  25947  dvlip2  25956  dv11cn  25962  deg1ldg  26053  deg1leb  26056  plycpn  26253  vieta1lem2  26275  elqaa  26286  aalioulem2  26297  aaliou3lem3  26308  aaliou3lem4  26310  pserulm  26387  psercnlem2  26390  psercnlem1  26391  psercn  26392  abelth  26407  reeff1o  26413  pilem1  26417  efhalfpi  26436  coseq0negpitopi  26468  pige3ALT  26485  tanregt0  26504  efif1olem3  26509  efif1olem4  26510  efifo  26512  eff1olem  26513  efsubm  26516  logrn  26523  ellogrn  26524  relogf1o  26531  argregt0  26575  argrege0  26576  dvrelog  26602  dvloglem  26613  logf1o2  26615  dvlog  26616  efopnlem1  26621  efopnlem2  26622  logtayl  26625  cxpcn3lem  26713  cxpcn3  26714  resqrtcn  26715  asinneg  26852  asinrebnd  26867  atan0  26874  atanbnd  26892  areambl  26924  sqrtlim  26939  amgmlem  26956  lgamucov  27004  basellem1  27047  basellem4  27050  sqff1o  27148  dchrplusg  27214  bposlem6  27256  bposlem8  27258  dchrvmasumlem2  27465  pntibndlem1  27556  pntlemo  27574  qrng0  27588  ostth  27606  noextendseq  27635  bday0  27807  oldlim  27883  ons2ind  28271  zsex  28376  lmif  28857  islmib  28859  structiedg0val  29095  snstriedgval  29111  umgredgnlp  29220  usgrexmplef  29332  usgrexmpledg  29335  vtxdlfgrval  29559  upgr2pthnlp  29805  konigsberglem5  30331  ex-mod  30524  pliguhgr  30561  grporn  30596  ip0i  30900  ubthlem1  30945  ubthlem2  30946  axhcompl-zf  31073  normlem7  31191  bcseqi  31195  bcsiALT  31254  hlimf  31312  hlimuni  31313  hhssabloilem  31336  hhshsslem1  31342  hhsssh  31344  hhsscms  31353  occllem  31378  occl  31379  h1deoi  31624  h1dei  31625  h1de2ctlem  31630  h1de2ci  31631  spansni  31632  spanunsni  31654  pjpythi  31797  nmfn0  32062  nmopadjlem  32164  adjcoi  32175  nmopcoadji  32176  pjoccoi  32253  shatomistici  32436  iuninc  32635  imadifxp  32676  xppreima  32723  1stpreima  32786  2ndpreima  32787  fsuppcurry1  32803  fsuppcurry2  32804  hashgt1  32888  s3clhash  33030  gsummpt2d  33132  xrge0tsmsd  33155  tocyc01  33200  cyc3evpm  33232  cycpmconjslem2  33237  cyc3conja  33239  reofld  33424  rearchi  33427  nn0archi  33428  xrge0slmod  33429  elrspunidl  33509  dimval  33757  dimvalfi  33758  ply1degltdimlem  33779  algextdeglem8  33881  qtophaus  33993  iistmd  34059  xpinpreima  34063  xpinpreima2  34064  tpr2rico  34069  mndpluscn  34083  xrge0pluscn  34097  cnzh  34125  rezh  34126  qqhucn  34149  rrhcn  34154  cnrrext  34167  zrhre  34176  qqhre  34177  ismntop  34183  sigaex  34267  brsiga  34340  cntnevol  34385  voliune  34386  ddemeas  34393  1stmbfm  34417  2ndmbfm  34418  br2base  34426  dya2icoseg2  34435  dya2iocucvr  34441  carsgclctunlem2  34476  carsgclctunlem3  34477  sitgaddlemb  34505  eulerpartlemt  34528  eulerpartgbij  34529  eulerpartlemmf  34532  eulerpartlemgvv  34533  eulerpartlemgf  34536  eulerpart  34539  sseqmw  34548  sseqf  34549  sseqp1  34552  fiblem  34555  fibp1  34558  dstrvprob  34629  coinflipspace  34638  coinfliprv  34640  coinflippv  34641  ballotlem1  34644  ballotlem8  34694  circlemethhgt  34800  r11  35250  r12  35251  onvf1od  35301  usgrcyclgt2v  35325  iccllysconn  35444  rellysconn  35445  satf00  35568  fmla0  35576  msrid  35739  dfrdg2  35987  dfrdg4  36145  imagesset  36147  elhf  36368  filnetlem3  36574  limsucncmpi  36639  bj-babygodel  36803  bj-idres  37361  taupilem3  37520  icoreresf  37553  icoreelrnab  37555  relowlssretop  37564  poimirlem3  37820  poimirlem9  37826  poimirlem15  37832  poimirlem16  37833  poimirlem17  37834  poimirlem19  37836  poimirlem27  37844  poimirlem28  37845  poimirlem31  37848  poimirlem32  37849  mblfinlem1  37854  ovoliunnfl  37859  voliunnfl  37861  mbfresfi  37863  dvtan  37867  itg2addnc  37871  ftc1anclem3  37892  areacirc  37910  fdc  37942  ismrer1  38035  reheibor  38036  rngomndo  38132  gidsn  38149  ac6s6f  38370  cnvref4  38539  dfcnvrefrels2  38777  dfcnvrefrels3  38778  dedths  39218  tendo0co2  41044  erng1r  41251  dvalveclem  41281  dva0g  41283  dvh0g  41367  sn-it0e0  42667  sn-0tie0  42702  2rexfrabdioph  43034  3rexfrabdioph  43035  4rexfrabdioph  43036  6rexfrabdioph  43037  7rexfrabdioph  43038  rencldnfi  43059  jm2.27dlem2  43248  wepwso  43281  dfac11  43300  pwssplit4  43327  frlmpwfi  43336  isnumbasgrplem3  43343  mpaaeu  43388  proot1mul  43432  proot1hash  43433  epirron  43492  oneptr  43493  ordeldif1o  43498  oaomoencom  43555  oenassex  43556  cnvcnvintabd  43837  cnvrcl0  43862  dfrtrcl5  43866  cotrcltrcl  43962  frege92  44192  seff  44546  prmunb2  44548  binomcxplemdvbinom  44590  binomcxplemcvg  44591  binomcxplemnotnn0  44593  permac8prim  45251  sumsnd  45267  islptre  45861  stoweidlem34  46274  stoweidlem37  46277  stirlinglem11  46324  stirlinglem12  46325  stirlinglem13  46326  fouriersw  46471  natlocalincr  47116  nthrucw  47126  fundcmpsurbijinjpreimafv  47649  fundcmpsurinjimaid  47653  fmtnoinf  47778  gbowge7  48005  nnsum3primes4  48030  usgrexmpl12ngrlic  48281  gpgprismgr4cycllem2  48338  gpg5ngric  48370  2zrng0  48486  lmodn0  48737  zlmodzxzldeplem3  48744  lvecpsslmod  48749  0dig2pr01  48852  nelsubc3lem  49311  aacllem  50042  amgmwlem  50043