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  1652  dtruALT2  5343  intasym  6117  relcoi2  6280  funres11  6615  cnvresid  6617  find  7893  fparlem1  8108  fparlem2  8109  dftpos4  8242  tposf12  8248  tfr2b  8384  tz7.44lem1  8393  ord3  8470  xp01disjl  8478  on2recsfn  8654  on2recsov  8655  on2ind  8656  on3ind  8657  xpcomco  9056  sbthlem2  9077  fidomdm  9292  brwdom2  9536  epnsym  9579  inf3lem6  9603  cnfcom  9670  ttrclco  9688  ttrclselem2  9696  tz9.1c  9700  frr1  9732  r1tr  9749  r1ord3g  9752  rankwflemb  9766  r1elwf  9769  r1elss  9779  rankval3b  9799  onssr1  9804  inlresf  9901  inrresf  9903  djuin  9905  infxpenlem  9998  alephnbtwn  10056  alephordilem1  10058  alephfp  10093  dfac13  10127  pwsdompw  10187  infdjuabs  10189  ackbij1  10221  ackbij2  10226  r1om  10227  cflim2  10248  fin23lem27  10313  fin23lem29  10326  fin23lem30  10327  fin1a2lem6  10390  fin1a2lem7  10391  fin1a2lem13  10397  itunitc1  10405  itunitc  10406  ituniiun  10407  hsmexlem5  10415  axcc2lem  10421  axcc3  10423  zorn2lem6  10486  zorn2lem7  10487  ttukeylem6  10499  dmct  10509  iunfo  10524  cardval  10531  cardid  10532  alephom  10571  canthp1lem2  10639  gchaleph2  10658  r1limwun  10722  inaprc  10822  nqerf  10916  recmulnq  10950  dmrecnq  10954  halfnq  10962  genpdm  10988  reclem3pr  11035  axresscn  11134  axpre-sup  11155  1re  11209  0re  11211  00id  11386  addrid  11391  0cnALT  11446  renegcli  11520  zexALT  12612  uzn0  12880  xrinfmss  13337  axdc4uzlem  14021  facnn  14313  fac0  14314  hashgval  14371  hashinf  14373  hashresfn  14378  hashrabrsn  14410  hashrabsn01  14411  hashrabsn1  14412  hashp1i  14441  hash1snb  14458  hashxplem  14472  fi1uzind  14546  cshw1  14861  cats1fv  14898  s7f1o  15005  trclubgi  15036  cnrecnv  15218  rexanuz  15399  climdm  15607  lo1eq  15621  rlimeq  15622  sumsnf  15796  tanval  16185  rpnnen2lem11  16281  rpnnen  16284  sadadd2lem  16518  sadadd3  16520  sadaddlem  16525  sadasslem  16529  sadeq  16531  lcmgcdlem  16665  unbenlem  16969  prmreclem6  16982  vdwlem8  17049  vdwnnlem1  17056  0ram  17081  structcnvcnv  17214  prdsvallem  17508  prdsval  17509  prdsbas  17511  prdsplusg  17512  prdsmulr  17513  prdsvsca  17514  prdshom  17521  xpsfrn  17623  xpsff1o2  17624  catcoppccl  18175  catcfuccl  18176  catcxpccl  18264  tsrss  18646  gsumpropd2lem  18738  smndex2dnrinv  18978  mvdco  19516  efgmnvl  19785  efgval  19788  efgi0  19791  efgi1  19792  efgredeu  19823  0frgp  19850  abln0  19938  lt6abl  19966  gsumval3  19978  gsum2dlem2  20042  dprdres  20101  dmdprdsplit2lem  20118  ringn0  20395  isdrng2  20830  drngid2  20838  cnfldplusf  21530  cnfldsub  21531  cnsubmlem  21546  cnsubglem  21547  cnmsubglem  21561  gzrngunitlem  21563  rge0srg  21569  zring0  21589  pzriprnglem10  21621  zzngim  21683  zrhpsgnmhm  21715  re0g  21743  pjfval  21837  pjpm  21839  psrplusg  22068  coe1sfi  22354  ply1plusgfvi  22382  marep01ma  22798  smadiadetlem1a  22801  smadiadetlem3lem2  22805  smadiadetlem3  22806  smadiadetlem4  22807  smadiadet  22808  indistpsALT  23151  tgrest  23297  leordtval2  23350  lmbr2  23397  cnprest  23427  lmff  23439  kgenidm  23685  tx1cn  23747  tx2cn  23748  ustbas  24365  psmetge0  24450  xmetge0  24482  qdensere  24907  cnblcld  24912  cnfldms  24913  cnfldtopn  24919  xrsdsre  24949  xrge0tsms  24973  iccpnfcnv  25084  xrhmeo  25086  cnheiborlem  25094  cnlmod  25280  recvs  25286  lmmbr2  25399  lmcau  25453  metsscmetcld  25455  cncms  25495  cnfldcusp  25497  ovolctb  25630  ovoliunnul  25647  ismbl  25666  volf  25669  voliunlem1  25690  ioorf  25713  ioorinv  25716  ioorcl  25717  dyaddisj  25736  dyadmax  25738  dyadmbl  25740  mbfid  25775  ismbfd  25779  mbfimaopnlem  25795  limcresi  26025  dvreslem  26049  dvres2lem  26050  dvcjbr  26089  dvferm1  26125  dvferm2  26127  dvlip2  26135  dv11cn  26141  deg1ldg  26230  deg1leb  26233  plycpn  26431  vieta1lem2  26453  elqaa  26464  aalioulem2  26475  aaliou3lem3  26486  aaliou3lem4  26488  pserulm  26563  psercnlem2  26565  psercnlem1  26566  psercn  26567  abelth  26582  reeff1o  26588  pilem1  26592  efhalfpi  26614  coseq0negpitopi  26646  pige3ALT  26663  tanregt0  26682  efif1olem3  26687  efif1olem4  26688  efifo  26690  eff1olem  26691  efsubm  26694  logrn  26701  ellogrn  26702  relogf1o  26709  argregt0  26753  argrege0  26754  dvrelog  26780  dvloglem  26791  logf1o2  26793  dvlog  26794  efopnlem1  26799  efopnlem2  26800  logtayl  26803  cxpcn3lem  26890  cxpcn3  26891  resqrtcn  26892  asinneg  27029  asinrebnd  27044  atan0  27051  atanbnd  27069  areambl  27101  sqrtlim  27115  amgmlem  27132  lgamucov  27180  basellem1  27223  basellem4  27226  sqff1o  27324  dchrplusg  27389  bposlem6  27431  bposlem8  27433  dchrvmasumlem2  27640  pntibndlem1  27731  pntlemo  27749  qrng0  27763  ostth  27781  noextendseq  27809  bday0  27982  oldlim  28058  ons2ind  28446  zsex  28551  lmif  29072  islmib  29074  structiedg0val  29350  snstriedgval  29366  umgredgnlp  29475  usgrexmplef  29587  usgrexmpledg  29590  vtxdlfgrval  29813  upgr2pthnlp  30059  konigsberglem5  30585  ex-mod  30778  nowisdomv  30803  pliguhgr  30816  grporn  30851  ip0i  31155  ubthlem1  31200  ubthlem2  31201  axhcompl-zf  31328  normlem7  31446  bcseqi  31450  bcsiALT  31509  hlimf  31567  hlimuni  31568  hhssabloilem  31591  hhshsslem1  31597  hhsssh  31599  hhsscms  31608  occllem  31633  occl  31634  h1deoi  31879  h1dei  31880  h1de2ctlem  31885  h1de2ci  31886  spansni  31887  spanunsni  31909  pjpythi  32052  nmfn0  32317  nmopadjlem  32419  adjcoi  32430  nmopcoadji  32431  pjoccoi  32508  shatomistici  32691  iuninc  32883  imadifxp  32924  xppreima  32968  1stpreima  33030  2ndpreima  33031  fsuppcurry1  33047  fsuppcurry2  33048  hashgt1  33131  s3clhash  33246  gsummpt2d  33347  xrge0tsmsd  33371  tocyc01  33416  cyc3evpm  33448  cycpmconjslem2  33453  cyc3conja  33455  reofld  33641  rearchi  33644  nn0archi  33645  xrge0slmod  33646  elrspunidl  33714  dimval  33969  dimvalfi  33970  ply1degltdimlem  33990  algextdeglem8  34092  qtophaus  34204  iistmd  34270  xpinpreima  34274  xpinpreima2  34275  tpr2rico  34280  mndpluscn  34294  xrge0pluscn  34308  cnzh  34336  rezh  34337  qqhucn  34360  rrhcn  34365  cnrrext  34378  zrhre  34387  qqhre  34388  ismntop  34394  sigaex  34478  brsiga  34551  cntnevol  34596  voliune  34597  ddemeas  34604  1stmbfm  34628  2ndmbfm  34629  br2base  34637  dya2icoseg2  34646  dya2iocucvr  34652  carsgclctunlem2  34687  carsgclctunlem3  34688  sitgaddlemb  34716  eulerpartlemt  34739  eulerpartgbij  34740  eulerpartlemmf  34743  eulerpartlemgvv  34744  eulerpartlemgf  34747  eulerpart  34750  sseqmw  34759  sseqf  34760  sseqp1  34763  fiblem  34766  fibp1  34769  dstrvprob  34840  coinflipspace  34849  coinfliprv  34851  coinflippv  34852  ballotlem1  34855  ballotlem8  34905  circlemethhgt  35008  r11  35465  r12  35466  onvf1od  35569  usgrcyclgt2v  35601  iccllysconn  35720  rellysconn  35721  satf00  35844  fmla0  35852  msrid  36015  dfrdg2  36263  dfrdg4  36421  imagesset  36423  elhf  36644  filnetlem3  36869  limsucncmpi  36934  ttciunun  37000  bj-babygodel  37174  bj-idres  37782  taupilem3  37941  icoreresf  37976  icoreelrnab  37978  relowlssretop  37987  poimirlem3  38252  poimirlem9  38258  poimirlem15  38264  poimirlem16  38265  poimirlem17  38266  poimirlem19  38268  poimirlem27  38276  poimirlem28  38277  poimirlem31  38280  poimirlem32  38281  mblfinlem1  38286  ovoliunnfl  38291  voliunnfl  38293  mbfresfi  38295  dvtan  38299  itg2addnc  38303  ftc1anclem3  38324  areacirc  38342  fdc  38374  ismrer1  38467  reheibor  38468  rngomndo  38564  gidsn  38581  ac6s6f  38800  cnvref4  38977  dfcnvrefrels2  39235  dfcnvrefrels3  39236  dedths  39714  tendo0co2  41540  erng1r  41747  dvalveclem  41777  dva0g  41779  dvh0g  41863  sn-it0e0  43155  sn-0tie0  43203  2rexfrabdioph  43503  3rexfrabdioph  43504  4rexfrabdioph  43505  6rexfrabdioph  43506  7rexfrabdioph  43507  rencldnfi  43528  jm2.27dlem2  43717  wepwso  43750  dfac11  43769  pwssplit4  43796  frlmpwfi  43805  isnumbasgrplem3  43812  mpaaeu  43857  proot1mul  43901  proot1hash  43902  epirron  43961  oneptr  43962  ordeldif1o  43967  oaomoencom  44024  oenassex  44025  cnvcnvintabd  44306  cnvrcl0  44331  dfrtrcl5  44335  cotrcltrcl  44431  frege92  44661  seff  44999  prmunb2  45001  binomcxplemdvbinom  45043  binomcxplemcvg  45044  binomcxplemnotnn0  45046  permac8prim  45703  sumsnd  45726  islptre  46315  stoweidlem34  46728  stoweidlem37  46731  stirlinglem11  46778  stirlinglem12  46779  stirlinglem13  46780  fouriersw  46925  natlocalincr  47572  nthrucw  47582  fundcmpsurbijinjpreimafv  48133  fundcmpsurinjimaid  48137  fmtnoinf  48265  gbowge7  48505  nnsum3primes4  48530  usgrexmpl12ngrlic  48781  gpgprismgr4cycllem2  48838  gpg5ngric  48870  2zrng0  48986  lmodn0  49252  zlmodzxzldeplem3  49259  lvecpsslmod  49264  0dig2pr01  49367  nelsubc3lem  49825  aacllem  50578  amgmwlem  50579