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  1625  nfcriOLD  2894  nfcriOLDOLD  2895  ceqsexv2d  3529  dtruALT2  5369  dtruOLD  5442  intasym  6117  relcoi2  6277  funres11  6626  cnvresid  6628  omsindsOLD  7877  find  7887  fparlem1  8098  fparlem2  8099  dftpos4  8230  tposf12  8236  wfrlem14OLD  8322  tfr2b  8396  tz7.44lem1  8405  ord3  8483  xp01disjl  8492  on2recsfn  8666  on2recsov  8667  on2ind  8668  on3ind  8669  xpcomco  9062  sbthlem2  9084  fidomdm  9329  brwdom2  9568  epnsym  9604  inf3lem6  9628  omex  9638  cnfcom  9695  ttrclco  9713  ttrclselem2  9721  tz9.1c  9725  frr1  9754  r1tr  9771  r1ord3g  9774  rankwflemb  9788  r1elwf  9791  r1elss  9801  rankval3b  9821  onssr1  9826  inlresf  9909  inrresf  9911  djuin  9913  infxpenlem  10008  alephnbtwn  10066  alephordilem1  10068  alephfp  10103  dfac13  10137  pwsdompw  10199  infdjuabs  10201  ackbij1  10233  ackbij2  10238  r1om  10239  cflim2  10258  fin23lem27  10323  fin23lem29  10336  fin23lem30  10337  fin1a2lem6  10400  fin1a2lem7  10401  fin1a2lem13  10407  itunitc1  10415  itunitc  10416  ituniiun  10417  hsmexlem5  10425  axcc2lem  10431  axcc3  10433  zorn2lem6  10496  zorn2lem7  10497  ttukeylem6  10509  axdc  10516  dmct  10519  iunfo  10534  cardval  10541  cardid  10542  pwcfsdom  10578  alephom  10580  canthp1lem2  10648  gchaleph2  10667  r1limwun  10731  inaprc  10831  nqerf  10925  recmulnq  10959  dmrecnq  10963  halfnq  10971  genpdm  10997  reclem3pr  11044  axresscn  11143  axpre-sup  11164  1re  11214  0re  11216  00id  11389  addrid  11394  0cnALT  11448  renegcli  11521  zexALT  12578  uzn0  12839  xrinfmss  13289  axdc4uzlem  13948  facnn  14235  fac0  14236  hashgval  14293  hashinf  14295  hashresfn  14300  hashrabrsn  14332  hashrabsn01  14333  hashrabsn1  14334  hashp1i  14363  hash1snb  14379  hashxplem  14393  fi1uzind  14458  cshw1  14772  cats1fv  14810  trclubgi  14944  cnrecnv  15112  rexanuz  15292  climdm  15498  lo1eq  15512  rlimeq  15513  sumsnf  15689  tanval  16071  rpnnen2lem11  16167  rpnnen  16170  sadadd2lem  16400  sadadd3  16402  sadaddlem  16407  sadasslem  16411  sadeq  16413  lcmgcdlem  16543  unbenlem  16841  prmreclem6  16854  vdwlem8  16921  vdwnnlem1  16928  0ram  16953  structcnvcnv  17086  prdsvallem  17400  prdsval  17401  prdsbas  17403  prdsplusg  17404  prdsmulr  17405  prdsvsca  17406  prdshom  17413  xpsfrn  17514  xpsff1o2  17515  catcoppccl  18067  catcoppcclOLD  18068  catcfuccl  18069  catcfucclOLD  18070  catcxpccl  18159  catcxpcclOLD  18160  tsrss  18542  gsumpropd2lem  18598  smndex2dnrinv  18796  mvdco  19313  efgmnvl  19582  efgval  19585  efgi0  19588  efgi1  19589  efgredeu  19620  0frgp  19647  abln0  19735  lt6abl  19763  gsumval3  19775  gsum2dlem2  19839  dprdres  19898  dmdprdsplit2lem  19915  ringn0  20123  isdrng2  20371  drngmcl  20374  drngid2  20378  cnfldplusf  20972  cnfldsub  20973  cnsubmlem  20993  cnsubglem  20994  cnmsubglem  21008  gzrngunitlem  21010  rge0srg  21016  zring0  21028  zzngim  21108  zrhpsgnmhm  21137  re0g  21165  pjfval  21261  pjpm  21263  psrplusg  21500  coe1sfi  21737  ply1plusgfvi  21764  marep01ma  22162  smadiadetlem1a  22165  smadiadetlem3lem2  22169  smadiadetlem3  22170  smadiadetlem4  22171  smadiadet  22172  indistpsALT  22516  indistpsALTOLD  22517  tgrest  22663  leordtval2  22716  lmbr2  22763  cnprest  22793  lmff  22805  kgenidm  23051  tx1cn  23113  tx2cn  23114  ustbas  23732  psmetge0  23818  xmetge0  23850  qdensere  24286  cnblcld  24291  cnfldms  24292  cnfldtopn  24298  xrsdsre  24326  xrge0tsms  24350  iccpnfcnv  24460  xrhmeo  24462  cnheiborlem  24470  cnlmod  24656  recvs  24662  lmmbr2  24776  lmcau  24830  metsscmetcld  24832  cncms  24872  cnfldcusp  24874  ovolctb  25007  ovoliunnul  25024  ismbl  25043  volf  25046  voliunlem1  25067  ioorf  25090  ioorinv  25093  ioorcl  25094  dyaddisj  25113  dyadmax  25115  dyadmbl  25117  mbfid  25152  ismbfd  25156  mbfimaopnlem  25172  limcresi  25402  dvreslem  25426  dvres2lem  25427  dvcjbr  25466  dvferm1  25502  dvferm2  25504  dvlip2  25512  dv11cn  25518  deg1ldg  25610  deg1leb  25613  plycpn  25802  vieta1lem2  25824  elqaa  25835  aalioulem2  25846  aaliou3lem3  25857  aaliou3lem4  25859  pserulm  25934  psercnlem2  25936  psercnlem1  25937  psercn  25938  abelth  25953  reeff1o  25959  pilem1  25963  efhalfpi  25981  coseq0negpitopi  26013  pige3ALT  26029  tanregt0  26048  efif1olem3  26053  efif1olem4  26054  efifo  26056  eff1olem  26057  efsubm  26060  logrn  26067  ellogrn  26068  relogf1o  26075  argregt0  26118  argrege0  26119  dvrelog  26145  dvloglem  26156  logf1o2  26158  dvlog  26159  efopnlem1  26164  efopnlem2  26165  logtayl  26168  cxpcn3lem  26255  cxpcn3  26256  resqrtcn  26257  asinneg  26391  asinrebnd  26406  atan0  26413  atanbnd  26431  areambl  26463  sqrtlim  26477  amgmlem  26494  lgamucov  26542  basellem1  26585  basellem4  26588  sqff1o  26686  dchrplusg  26750  bposlem6  26792  bposlem8  26794  dchrvmasumlem2  27001  mulog2sum  27040  pntibndlem1  27092  pntlemo  27110  qrng0  27124  ostth  27142  noextendseq  27170  bday0s  27329  oldlim  27381  lmif  28036  islmib  28038  structiedg0val  28282  snstriedgval  28298  umgredgnlp  28407  usgrexmplef  28516  usgrexmpledg  28519  vtxdlfgrval  28742  upgr2pthnlp  28989  konigsberglem5  29509  ex-mod  29702  pliguhgr  29739  grporn  29774  ip0i  30078  ubthlem1  30123  ubthlem2  30124  axhcompl-zf  30251  normlem7  30369  bcseqi  30373  bcsiALT  30432  hlimf  30490  hlimuni  30491  hhssabloilem  30514  hhshsslem1  30520  hhsssh  30522  hhsscms  30531  occllem  30556  occl  30557  h1deoi  30802  h1dei  30803  h1de2ctlem  30808  h1de2ci  30809  spansni  30810  spanunsni  30832  pjpythi  30975  nmfn0  31240  nmopadjlem  31342  adjcoi  31353  nmopcoadji  31354  pjoccoi  31431  shatomistici  31614  iuninc  31792  imadifxp  31832  xppreima  31871  1stpreima  31928  2ndpreima  31929  fsuppcurry1  31950  fsuppcurry2  31951  hashgt1  32020  s3clhash  32114  gsummpt2d  32201  xrge0tsmsd  32209  tocyc01  32277  cyc3evpm  32309  cycpmconjslem2  32314  cyc3conja  32316  reofld  32459  rearchi  32461  nn0archi  32462  xrge0slmod  32463  elrspunidl  32546  dimval  32686  dimvalfi  32687  ply1degltdimlem  32707  qtophaus  32816  iistmd  32882  xpinpreima  32886  xpinpreima2  32887  tpr2rico  32892  mndpluscn  32906  xrge0pluscn  32920  cnzh  32950  rezh  32951  qqhucn  32972  rrhcn  32977  cnrrext  32990  zrhre  32999  qqhre  33000  ismntop  33006  sigaex  33108  brsiga  33181  cntnevol  33226  voliune  33227  ddemeas  33234  1stmbfm  33259  2ndmbfm  33260  br2base  33268  dya2icoseg2  33277  dya2iocucvr  33283  carsgclctunlem2  33318  carsgclctunlem3  33319  sitgaddlemb  33347  eulerpartlemt  33370  eulerpartgbij  33371  eulerpartlemmf  33374  eulerpartlemgvv  33375  eulerpartlemgf  33378  eulerpart  33381  sseqmw  33390  sseqf  33391  sseqp1  33394  fiblem  33397  fibp1  33400  dstrvprob  33470  coinflipspace  33479  coinfliprv  33481  coinflippv  33482  ballotlem1  33485  ballotlem8  33535  circlemethhgt  33655  usgrcyclgt2v  34122  iccllysconn  34241  rellysconn  34242  satf00  34365  fmla0  34373  msrid  34536  dfrdg2  34767  dfrdg4  34923  imagesset  34925  elhf  35146  filnetlem3  35265  limsucncmpi  35330  bj-babygodel  35481  bj-idres  36041  taupilem3  36200  icoreresf  36233  icoreelrnab  36235  relowlssretop  36244  poimirlem3  36491  poimirlem9  36497  poimirlem15  36503  poimirlem16  36504  poimirlem17  36505  poimirlem19  36507  poimirlem27  36515  poimirlem28  36516  poimirlem31  36519  poimirlem32  36520  mblfinlem1  36525  ovoliunnfl  36530  voliunnfl  36532  mbfresfi  36534  dvtan  36538  itg2addnc  36542  ftc1anclem3  36563  areacirc  36581  fdc  36613  ismrer1  36706  reheibor  36707  rngomndo  36803  gidsn  36820  ac6s6f  37041  eccnvepex  37204  cnvref4  37219  dfcnvrefrels2  37398  dfcnvrefrels3  37399  dedths  37832  tendo0co2  39659  erng1r  39866  dvalveclem  39896  dva0g  39898  dvh0g  39982  sn-it0e0  41288  sn-0tie0  41312  2rexfrabdioph  41534  3rexfrabdioph  41535  4rexfrabdioph  41536  6rexfrabdioph  41537  7rexfrabdioph  41538  rencldnfi  41559  jm2.27dlem2  41749  wepwso  41785  dfac11  41804  pwssplit4  41831  frlmpwfi  41840  isnumbasgrplem3  41847  mpaaeu  41892  proot1mul  41941  proot1hash  41942  epirron  42003  oneptr  42004  ordeldif1o  42010  oaomoencom  42067  oenassex  42068  cnvcnvintabd  42351  cnvrcl0  42376  dfrtrcl5  42380  cotrcltrcl  42476  frege92  42706  seff  43068  prmunb2  43070  binomcxplemdvbinom  43112  binomcxplemcvg  43113  binomcxplemnotnn0  43115  sumsnd  43710  islptre  44335  stoweidlem34  44750  stoweidlem37  44753  stirlinglem11  44800  stirlinglem12  44801  stirlinglem13  44802  fouriersw  44947  natlocalincr  45590  upwordsing  45598  fundcmpsurbijinjpreimafv  46075  fundcmpsurinjimaid  46079  fmtnoinf  46204  gbowge7  46431  nnsum3primes4  46456  pzriprnglem10  46814  2zrng0  46836  lmodn0  47176  zlmodzxzldeplem3  47183  lvecpsslmod  47188  0dig2pr01  47296  aacllem  47848  amgmwlem  47849