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  2895  nfcriOLDOLD  2896  ceqsexv2d  3493  dtruALT2  5317  dtruOLD  5390  intasym  6059  relcoi2  6219  funres11  6565  cnvresid  6567  omsindsOLD  7806  find  7815  fparlem1  8024  fparlem2  8025  dftpos4  8135  tposf12  8141  wfrlem14OLD  8227  tfr2b  8301  tz7.44lem1  8310  ord3  8388  xp01disjl  8397  xpcomco  8931  sbthlem2  8953  fidomdm  9198  brwdom2  9434  epnsym  9470  inf3lem6  9494  omex  9504  cnfcom  9561  ttrclco  9579  ttrclselem2  9587  tz9.1c  9591  frr1  9620  r1tr  9637  r1ord3g  9640  rankwflemb  9654  r1elwf  9657  r1elss  9667  rankval3b  9687  onssr1  9692  inlresf  9775  inrresf  9777  djuin  9779  infxpenlem  9874  alephnbtwn  9932  alephordilem1  9934  alephfp  9969  dfac13  10003  pwsdompw  10065  infdjuabs  10067  ackbij1  10099  ackbij2  10104  r1om  10105  cflim2  10124  fin23lem27  10189  fin23lem29  10202  fin23lem30  10203  fin1a2lem6  10266  fin1a2lem7  10267  fin1a2lem13  10273  itunitc1  10281  itunitc  10282  ituniiun  10283  hsmexlem5  10291  axcc2lem  10297  axcc3  10299  zorn2lem6  10362  zorn2lem7  10363  ttukeylem6  10375  axdc  10382  dmct  10385  iunfo  10400  cardval  10407  cardid  10408  pwcfsdom  10444  alephom  10446  canthp1lem2  10514  gchaleph2  10533  r1limwun  10597  inaprc  10697  nqerf  10791  recmulnq  10825  dmrecnq  10829  halfnq  10837  genpdm  10863  reclem3pr  10910  axresscn  11009  axpre-sup  11030  1re  11080  0re  11082  00id  11255  addid1  11260  0cnALT  11314  renegcli  11387  zexALT  12444  uzn0  12704  xrinfmss  13149  axdc4uzlem  13808  facnn  14094  fac0  14095  hashgval  14152  hashinf  14154  hashresfn  14159  hashrabrsn  14191  hashrabsn01  14192  hashrabsn1  14193  hashp1i  14222  hash1snb  14238  hashxplem  14252  fi1uzind  14315  cshw1  14633  cats1fv  14671  trclubgi  14807  cnrecnv  14975  rexanuz  15156  climdm  15362  lo1eq  15376  rlimeq  15377  sumsnf  15554  tanval  15936  rpnnen2lem11  16032  rpnnen  16035  sadadd2lem  16265  sadadd3  16267  sadaddlem  16272  sadasslem  16276  sadeq  16278  lcmgcdlem  16408  unbenlem  16706  prmreclem6  16719  vdwlem8  16786  vdwnnlem1  16793  0ram  16818  structcnvcnv  16951  prdsvallem  17262  prdsval  17263  prdsbas  17265  prdsplusg  17266  prdsmulr  17267  prdsvsca  17268  prdshom  17275  xpsfrn  17376  xpsff1o2  17377  catcoppccl  17929  catcoppcclOLD  17930  catcfuccl  17931  catcfucclOLD  17932  catcxpccl  18021  catcxpcclOLD  18022  tsrss  18404  gsumpropd2lem  18460  smndex2dnrinv  18650  mvdco  19149  efgmnvl  19415  efgval  19418  efgi0  19421  efgi1  19422  efgredeu  19453  0frgp  19480  abln0  19563  lt6abl  19590  gsumval3  19602  gsum2dlem2  19666  dprdres  19725  dmdprdsplit2lem  19742  ringn0  19936  isdrng2  20105  drngmcl  20108  drngid2  20111  cnfldplusf  20730  cnfldsub  20731  cnsubmlem  20751  cnsubglem  20752  cnmsubglem  20766  gzrngunitlem  20768  rge0srg  20774  zring0  20785  zzngim  20865  zrhpsgnmhm  20894  re0g  20922  pjfval  21018  pjpm  21020  psrplusg  21255  coe1sfi  21489  ply1plusgfvi  21518  marep01ma  21914  smadiadetlem1a  21917  smadiadetlem3lem2  21921  smadiadetlem3  21922  smadiadetlem4  21923  smadiadet  21924  indistpsALT  22268  indistpsALTOLD  22269  tgrest  22415  leordtval2  22468  lmbr2  22515  cnprest  22545  lmff  22557  kgenidm  22803  tx1cn  22865  tx2cn  22866  ustbas  23484  psmetge0  23570  xmetge0  23602  qdensere  24038  cnblcld  24043  cnfldms  24044  cnfldtopn  24050  xrsdsre  24078  xrge0tsms  24102  iccpnfcnv  24212  xrhmeo  24214  cnheiborlem  24222  cnlmod  24408  recvs  24414  lmmbr2  24528  lmcau  24582  metsscmetcld  24584  cncms  24624  cnfldcusp  24626  ovolctb  24759  ovoliunnul  24776  ismbl  24795  volf  24798  voliunlem1  24819  ioorf  24842  ioorinv  24845  ioorcl  24846  dyaddisj  24865  dyadmax  24867  dyadmbl  24869  mbfid  24904  ismbfd  24908  mbfimaopnlem  24924  limcresi  25154  dvreslem  25178  dvres2lem  25179  dvcjbr  25218  dvferm1  25254  dvferm2  25256  dvlip2  25264  dv11cn  25270  deg1ldg  25362  deg1leb  25365  plycpn  25554  vieta1lem2  25576  elqaa  25587  aalioulem2  25598  aaliou3lem3  25609  aaliou3lem4  25611  pserulm  25686  psercnlem2  25688  psercnlem1  25689  psercn  25690  abelth  25705  reeff1o  25711  pilem1  25715  efhalfpi  25733  coseq0negpitopi  25765  pige3ALT  25781  tanregt0  25800  efif1olem3  25805  efif1olem4  25806  efifo  25808  eff1olem  25809  efsubm  25812  logrn  25819  ellogrn  25820  relogf1o  25827  argregt0  25870  argrege0  25871  dvrelog  25897  dvloglem  25908  logf1o2  25910  dvlog  25911  efopnlem1  25916  efopnlem2  25917  logtayl  25920  cxpcn3lem  26005  cxpcn3  26006  resqrtcn  26007  asinneg  26141  asinrebnd  26156  atan0  26163  atanbnd  26181  areambl  26213  sqrtlim  26227  amgmlem  26244  lgamucov  26292  basellem1  26335  basellem4  26338  sqff1o  26436  dchrplusg  26500  bposlem6  26542  bposlem8  26544  dchrvmasumlem2  26751  mulog2sum  26790  pntibndlem1  26842  pntlemo  26860  qrng0  26874  ostth  26892  noextendseq  26920  bday0s  27072  lmif  27434  islmib  27436  structiedg0val  27680  snstriedgval  27696  umgredgnlp  27805  usgrexmplef  27914  usgrexmpledg  27917  vtxdlfgrval  28140  upgr2pthnlp  28387  konigsberglem5  28907  ex-mod  29100  pliguhgr  29135  grporn  29170  ip0i  29474  ubthlem1  29519  ubthlem2  29520  axhcompl-zf  29647  normlem7  29765  bcseqi  29769  bcsiALT  29828  hlimf  29886  hlimuni  29887  hhssabloilem  29910  hhshsslem1  29916  hhsssh  29918  hhsscms  29927  occllem  29952  occl  29953  h1deoi  30198  h1dei  30199  h1de2ctlem  30204  h1de2ci  30205  spansni  30206  spanunsni  30228  pjpythi  30371  nmfn0  30636  nmopadjlem  30738  adjcoi  30749  nmopcoadji  30750  pjoccoi  30827  shatomistici  31010  iuninc  31185  imadifxp  31225  xppreima  31268  1stpreima  31324  2ndpreima  31325  fsuppcurry1  31345  fsuppcurry2  31346  hashgt1  31413  s3clhash  31507  gsummpt2d  31594  xrge0tsmsd  31602  tocyc01  31670  cyc3evpm  31702  cycpmconjslem2  31707  cyc3conja  31709  reofld  31838  rearchi  31840  nn0archi  31841  xrge0slmod  31842  elrspunidl  31901  dimval  31982  dimvalfi  31983  qtophaus  32082  iistmd  32148  xpinpreima  32152  xpinpreima2  32153  tpr2rico  32158  mndpluscn  32172  xrge0pluscn  32186  cnzh  32216  rezh  32217  qqhucn  32238  rrhcn  32243  cnrrext  32256  zrhre  32265  qqhre  32266  ismntop  32272  sigaex  32374  brsiga  32447  cntnevol  32492  voliune  32493  ddemeas  32500  1stmbfm  32525  2ndmbfm  32526  br2base  32534  dya2icoseg2  32543  dya2iocucvr  32549  carsgclctunlem2  32584  carsgclctunlem3  32585  sitgaddlemb  32613  eulerpartlemt  32636  eulerpartgbij  32637  eulerpartlemmf  32640  eulerpartlemgvv  32641  eulerpartlemgf  32644  eulerpart  32647  sseqmw  32656  sseqf  32657  sseqp1  32660  fiblem  32663  fibp1  32666  dstrvprob  32736  coinflipspace  32745  coinfliprv  32747  coinflippv  32748  ballotlem1  32751  ballotlem8  32801  circlemethhgt  32921  usgrcyclgt2v  33390  iccllysconn  33509  rellysconn  33510  satf00  33633  fmla0  33641  msrid  33804  dfrdg2  34054  on2recsfn  34105  on2recsov  34106  on2ind  34107  on3ind  34108  oldlim  34177  dfrdg4  34390  imagesset  34392  elhf  34613  filnetlem3  34706  limsucncmpi  34771  bj-babygodel  34922  bj-idres  35485  taupilem3  35644  icoreresf  35677  icoreelrnab  35679  relowlssretop  35688  poimirlem3  35936  poimirlem9  35942  poimirlem15  35948  poimirlem16  35949  poimirlem17  35950  poimirlem19  35952  poimirlem27  35960  poimirlem28  35961  poimirlem31  35964  poimirlem32  35965  mblfinlem1  35970  ovoliunnfl  35975  voliunnfl  35977  mbfresfi  35979  dvtan  35983  itg2addnc  35987  ftc1anclem3  36008  areacirc  36026  fdc  36059  ismrer1  36152  reheibor  36153  rngomndo  36249  gidsn  36266  ac6s6f  36487  eccnvepex  36652  cnvref4  36667  dfcnvrefrels2  36846  dfcnvrefrels3  36847  dedths  37280  tendo0co2  39107  erng1r  39314  dvalveclem  39344  dva0g  39346  dvh0g  39430  sn-it0e0  40708  sn-0tie0  40732  2rexfrabdioph  40931  3rexfrabdioph  40932  4rexfrabdioph  40933  6rexfrabdioph  40934  7rexfrabdioph  40935  rencldnfi  40956  jm2.27dlem2  41146  wepwso  41182  dfac11  41201  pwssplit4  41228  frlmpwfi  41237  isnumbasgrplem3  41244  mpaaeu  41289  proot1mul  41338  proot1hash  41339  cnvcnvintabd  41581  cnvrcl0  41606  dfrtrcl5  41610  cotrcltrcl  41706  frege92  41936  seff  42300  prmunb2  42302  binomcxplemdvbinom  42344  binomcxplemcvg  42345  binomcxplemnotnn0  42347  sumsnd  42942  islptre  43548  stoweidlem34  43963  stoweidlem37  43966  stirlinglem11  44013  stirlinglem12  44014  stirlinglem13  44015  fouriersw  44160  natlocalincr  44793  upwordsing  44801  fundcmpsurbijinjpreimafv  45277  fundcmpsurinjimaid  45281  fmtnoinf  45406  gbowge7  45633  nnsum3primes4  45658  2zrng0  45914  lmodn0  46254  zlmodzxzldeplem3  46261  lvecpsslmod  46266  0dig2pr01  46374  aacllem  46923  amgmwlem  46924