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  1618  ceqsexv2dOLD  3533  dtruALT2  5375  dtruOLD  5451  intasym  6137  relcoi2  6298  funres11  6644  cnvresid  6646  omsindsOLD  7908  find  7917  fparlem1  8135  fparlem2  8136  dftpos4  8268  tposf12  8274  wfrlem14OLD  8360  tfr2b  8434  tz7.44lem1  8443  ord3  8521  xp01disjl  8528  on2recsfn  8703  on2recsov  8704  on2ind  8705  on3ind  8706  xpcomco  9100  sbthlem2  9122  fidomdm  9371  brwdom2  9610  epnsym  9646  inf3lem6  9670  omex  9680  cnfcom  9737  ttrclco  9755  ttrclselem2  9763  tz9.1c  9767  frr1  9796  r1tr  9813  r1ord3g  9816  rankwflemb  9830  r1elwf  9833  r1elss  9843  rankval3b  9863  onssr1  9868  inlresf  9951  inrresf  9953  djuin  9955  infxpenlem  10050  alephnbtwn  10108  alephordilem1  10110  alephfp  10145  dfac13  10180  pwsdompw  10240  infdjuabs  10242  ackbij1  10274  ackbij2  10279  r1om  10280  cflim2  10300  fin23lem27  10365  fin23lem29  10378  fin23lem30  10379  fin1a2lem6  10442  fin1a2lem7  10443  fin1a2lem13  10449  itunitc1  10457  itunitc  10458  ituniiun  10459  hsmexlem5  10467  axcc2lem  10473  axcc3  10475  zorn2lem6  10538  zorn2lem7  10539  ttukeylem6  10551  axdc  10558  dmct  10561  iunfo  10576  cardval  10583  cardid  10584  pwcfsdom  10620  alephom  10622  canthp1lem2  10690  gchaleph2  10709  r1limwun  10773  inaprc  10873  nqerf  10967  recmulnq  11001  dmrecnq  11005  halfnq  11013  genpdm  11039  reclem3pr  11086  axresscn  11185  axpre-sup  11206  1re  11258  0re  11260  00id  11433  addrid  11438  0cnALT  11493  renegcli  11567  zexALT  12630  uzn0  12892  xrinfmss  13348  axdc4uzlem  14020  facnn  14310  fac0  14311  hashgval  14368  hashinf  14370  hashresfn  14375  hashrabrsn  14407  hashrabsn01  14408  hashrabsn1  14409  hashp1i  14438  hash1snb  14454  hashxplem  14468  fi1uzind  14542  cshw1  14856  cats1fv  14894  s7f1o  15001  trclubgi  15032  cnrecnv  15200  rexanuz  15380  climdm  15586  lo1eq  15600  rlimeq  15601  sumsnf  15775  tanval  16160  rpnnen2lem11  16256  rpnnen  16259  sadadd2lem  16492  sadadd3  16494  sadaddlem  16499  sadasslem  16503  sadeq  16505  lcmgcdlem  16639  unbenlem  16941  prmreclem6  16954  vdwlem8  17021  vdwnnlem1  17028  0ram  17053  structcnvcnv  17186  prdsvallem  17500  prdsval  17501  prdsbas  17503  prdsplusg  17504  prdsmulr  17505  prdsvsca  17506  prdshom  17513  xpsfrn  17614  xpsff1o2  17615  catcoppccl  18170  catcoppcclOLD  18171  catcfuccl  18172  catcfucclOLD  18173  catcxpccl  18262  catcxpcclOLD  18263  tsrss  18646  gsumpropd2lem  18704  smndex2dnrinv  18940  mvdco  19477  efgmnvl  19746  efgval  19749  efgi0  19752  efgi1  19753  efgredeu  19784  0frgp  19811  abln0  19899  lt6abl  19927  gsumval3  19939  gsum2dlem2  20003  dprdres  20062  dmdprdsplit2lem  20079  ringn0  20324  isdrng2  20759  drngmclOLD  20767  drngid2  20768  cnfldplusf  21426  cnfldsub  21427  cnsubmlem  21449  cnsubglem  21450  cnmsubglem  21465  gzrngunitlem  21467  rge0srg  21473  zring0  21486  pzriprnglem10  21518  zzngim  21588  zrhpsgnmhm  21619  re0g  21647  pjfval  21743  pjpm  21745  psrplusg  21973  coe1sfi  22230  ply1plusgfvi  22258  marep01ma  22681  smadiadetlem1a  22684  smadiadetlem3lem2  22688  smadiadetlem3  22689  smadiadetlem4  22690  smadiadet  22691  indistpsALT  23035  indistpsALTOLD  23036  tgrest  23182  leordtval2  23235  lmbr2  23282  cnprest  23312  lmff  23324  kgenidm  23570  tx1cn  23632  tx2cn  23633  ustbas  24251  psmetge0  24337  xmetge0  24369  qdensere  24805  cnblcld  24810  cnfldms  24811  cnfldtopn  24817  xrsdsre  24845  xrge0tsms  24869  iccpnfcnv  24988  xrhmeo  24990  cnheiborlem  24999  cnlmod  25186  recvs  25192  lmmbr2  25306  lmcau  25360  metsscmetcld  25362  cncms  25402  cnfldcusp  25404  ovolctb  25538  ovoliunnul  25555  ismbl  25574  volf  25577  voliunlem1  25598  ioorf  25621  ioorinv  25624  ioorcl  25625  dyaddisj  25644  dyadmax  25646  dyadmbl  25648  mbfid  25683  ismbfd  25687  mbfimaopnlem  25703  limcresi  25934  dvreslem  25958  dvres2lem  25959  dvcjbr  26001  dvferm1  26037  dvferm2  26039  dvlip2  26048  dv11cn  26054  deg1ldg  26145  deg1leb  26148  plycpn  26345  vieta1lem2  26367  elqaa  26378  aalioulem2  26389  aaliou3lem3  26400  aaliou3lem4  26402  pserulm  26479  psercnlem2  26482  psercnlem1  26483  psercn  26484  abelth  26499  reeff1o  26505  pilem1  26509  efhalfpi  26527  coseq0negpitopi  26559  pige3ALT  26576  tanregt0  26595  efif1olem3  26600  efif1olem4  26601  efifo  26603  eff1olem  26604  efsubm  26607  logrn  26614  ellogrn  26615  relogf1o  26622  argregt0  26666  argrege0  26667  dvrelog  26693  dvloglem  26704  logf1o2  26706  dvlog  26707  efopnlem1  26712  efopnlem2  26713  logtayl  26716  cxpcn3lem  26804  cxpcn3  26805  resqrtcn  26806  asinneg  26943  asinrebnd  26958  atan0  26965  atanbnd  26983  areambl  27015  sqrtlim  27030  amgmlem  27047  lgamucov  27095  basellem1  27138  basellem4  27141  sqff1o  27239  dchrplusg  27305  bposlem6  27347  bposlem8  27349  dchrvmasumlem2  27556  mulog2sum  27595  pntibndlem1  27647  pntlemo  27665  qrng0  27679  ostth  27697  noextendseq  27726  bday0s  27887  oldlim  27939  zsex  28380  lmif  28807  islmib  28809  structiedg0val  29053  snstriedgval  29069  umgredgnlp  29178  usgrexmplef  29290  usgrexmpledg  29293  vtxdlfgrval  29517  upgr2pthnlp  29764  konigsberglem5  30284  ex-mod  30477  pliguhgr  30514  grporn  30549  ip0i  30853  ubthlem1  30898  ubthlem2  30899  axhcompl-zf  31026  normlem7  31144  bcseqi  31148  bcsiALT  31207  hlimf  31265  hlimuni  31266  hhssabloilem  31289  hhshsslem1  31295  hhsssh  31297  hhsscms  31306  occllem  31331  occl  31332  h1deoi  31577  h1dei  31578  h1de2ctlem  31583  h1de2ci  31584  spansni  31585  spanunsni  31607  pjpythi  31750  nmfn0  32015  nmopadjlem  32117  adjcoi  32128  nmopcoadji  32129  pjoccoi  32206  shatomistici  32389  iuninc  32580  imadifxp  32620  xppreima  32661  1stpreima  32721  2ndpreima  32722  fsuppcurry1  32742  fsuppcurry2  32743  hashgt1  32817  s3clhash  32916  gsummpt2d  33034  xrge0tsmsd  33047  tocyc01  33120  cyc3evpm  33152  cycpmconjslem2  33157  cyc3conja  33159  reofld  33351  rearchi  33353  nn0archi  33354  xrge0slmod  33355  elrspunidl  33435  dimval  33627  dimvalfi  33628  ply1degltdimlem  33649  algextdeglem8  33729  qtophaus  33796  iistmd  33862  xpinpreima  33866  xpinpreima2  33867  tpr2rico  33872  mndpluscn  33886  xrge0pluscn  33900  cnzh  33930  rezh  33931  qqhucn  33954  rrhcn  33959  cnrrext  33972  zrhre  33981  qqhre  33982  ismntop  33988  sigaex  34090  brsiga  34163  cntnevol  34208  voliune  34209  ddemeas  34216  1stmbfm  34241  2ndmbfm  34242  br2base  34250  dya2icoseg2  34259  dya2iocucvr  34265  carsgclctunlem2  34300  carsgclctunlem3  34301  sitgaddlemb  34329  eulerpartlemt  34352  eulerpartgbij  34353  eulerpartlemmf  34356  eulerpartlemgvv  34357  eulerpartlemgf  34360  eulerpart  34363  sseqmw  34372  sseqf  34373  sseqp1  34376  fiblem  34379  fibp1  34382  dstrvprob  34452  coinflipspace  34461  coinfliprv  34463  coinflippv  34464  ballotlem1  34467  ballotlem8  34517  circlemethhgt  34636  usgrcyclgt2v  35115  iccllysconn  35234  rellysconn  35235  satf00  35358  fmla0  35366  msrid  35529  dfrdg2  35776  dfrdg4  35932  imagesset  35934  elhf  36155  filnetlem3  36362  limsucncmpi  36427  bj-babygodel  36585  bj-idres  37142  taupilem3  37301  icoreresf  37334  icoreelrnab  37336  relowlssretop  37345  poimirlem3  37609  poimirlem9  37615  poimirlem15  37621  poimirlem16  37622  poimirlem17  37623  poimirlem19  37625  poimirlem27  37633  poimirlem28  37634  poimirlem31  37637  poimirlem32  37638  mblfinlem1  37643  ovoliunnfl  37648  voliunnfl  37650  mbfresfi  37652  dvtan  37656  itg2addnc  37660  ftc1anclem3  37681  areacirc  37699  fdc  37731  ismrer1  37824  reheibor  37825  rngomndo  37921  gidsn  37938  ac6s6f  38159  eccnvepex  38316  cnvref4  38331  dfcnvrefrels2  38509  dfcnvrefrels3  38510  dedths  38943  tendo0co2  40770  erng1r  40977  dvalveclem  41007  dva0g  41009  dvh0g  41093  readvrec  42370  sn-it0e0  42421  sn-0tie0  42445  2rexfrabdioph  42783  3rexfrabdioph  42784  4rexfrabdioph  42785  6rexfrabdioph  42786  7rexfrabdioph  42787  rencldnfi  42808  jm2.27dlem2  42998  wepwso  43031  dfac11  43050  pwssplit4  43077  frlmpwfi  43086  isnumbasgrplem3  43093  mpaaeu  43138  proot1mul  43182  proot1hash  43183  epirron  43242  oneptr  43243  ordeldif1o  43249  oaomoencom  43306  oenassex  43307  cnvcnvintabd  43589  cnvrcl0  43614  dfrtrcl5  43618  cotrcltrcl  43714  frege92  43944  seff  44304  prmunb2  44306  binomcxplemdvbinom  44348  binomcxplemcvg  44349  binomcxplemnotnn0  44351  sumsnd  44963  islptre  45574  stoweidlem34  45989  stoweidlem37  45992  stirlinglem11  46039  stirlinglem12  46040  stirlinglem13  46041  fouriersw  46186  natlocalincr  46829  upwordsing  46837  fundcmpsurbijinjpreimafv  47331  fundcmpsurinjimaid  47335  fmtnoinf  47460  gbowge7  47687  nnsum3primes4  47712  usgrexmpl12ngrlic  47933  2zrng0  48087  lmodn0  48340  zlmodzxzldeplem3  48347  lvecpsslmod  48352  0dig2pr01  48459  aacllem  49031  amgmwlem  49032