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  1622  ceqsexv2dOLD  3500  dtruALT2  5325  dtruOLD  5401  intasym  6088  relcoi2  6250  funres11  6593  cnvresid  6595  find  7871  fparlem1  8091  fparlem2  8092  dftpos4  8224  tposf12  8230  tfr2b  8364  tz7.44lem1  8373  ord3  8449  xp01disjl  8456  on2recsfn  8631  on2recsov  8632  on2ind  8633  on3ind  8634  xpcomco  9031  sbthlem2  9052  fidomdm  9285  brwdom2  9526  epnsym  9562  inf3lem6  9586  cnfcom  9653  ttrclco  9671  ttrclselem2  9679  tz9.1c  9683  frr1  9712  r1tr  9729  r1ord3g  9732  rankwflemb  9746  r1elwf  9749  r1elss  9759  rankval3b  9779  onssr1  9784  inlresf  9867  inrresf  9869  djuin  9871  infxpenlem  9966  alephnbtwn  10024  alephordilem1  10026  alephfp  10061  dfac13  10096  pwsdompw  10156  infdjuabs  10158  ackbij1  10190  ackbij2  10195  r1om  10196  cflim2  10216  fin23lem27  10281  fin23lem29  10294  fin23lem30  10295  fin1a2lem6  10358  fin1a2lem7  10359  fin1a2lem13  10365  itunitc1  10373  itunitc  10374  ituniiun  10375  hsmexlem5  10383  axcc2lem  10389  axcc3  10391  zorn2lem6  10454  zorn2lem7  10455  ttukeylem6  10467  dmct  10477  iunfo  10492  cardval  10499  cardid  10500  alephom  10538  canthp1lem2  10606  gchaleph2  10625  r1limwun  10689  inaprc  10789  nqerf  10883  recmulnq  10917  dmrecnq  10921  halfnq  10929  genpdm  10955  reclem3pr  11002  axresscn  11101  axpre-sup  11122  1re  11174  0re  11176  00id  11349  addrid  11354  0cnALT  11409  renegcli  11483  zexALT  12549  uzn0  12810  xrinfmss  13270  axdc4uzlem  13948  facnn  14240  fac0  14241  hashgval  14298  hashinf  14300  hashresfn  14305  hashrabrsn  14337  hashrabsn01  14338  hashrabsn1  14339  hashp1i  14368  hash1snb  14384  hashxplem  14398  fi1uzind  14472  cshw1  14787  cats1fv  14825  s7f1o  14932  trclubgi  14963  cnrecnv  15131  rexanuz  15312  climdm  15520  lo1eq  15534  rlimeq  15535  sumsnf  15709  tanval  16096  rpnnen2lem11  16192  rpnnen  16195  sadadd2lem  16429  sadadd3  16431  sadaddlem  16436  sadasslem  16440  sadeq  16442  lcmgcdlem  16576  unbenlem  16879  prmreclem6  16892  vdwlem8  16959  vdwnnlem1  16966  0ram  16991  structcnvcnv  17123  prdsvallem  17417  prdsval  17418  prdsbas  17420  prdsplusg  17421  prdsmulr  17422  prdsvsca  17423  prdshom  17430  xpsfrn  17531  xpsff1o2  17532  catcoppccl  18079  catcfuccl  18080  catcxpccl  18168  tsrss  18548  gsumpropd2lem  18606  smndex2dnrinv  18842  mvdco  19375  efgmnvl  19644  efgval  19647  efgi0  19650  efgi1  19651  efgredeu  19682  0frgp  19709  abln0  19797  lt6abl  19825  gsumval3  19837  gsum2dlem2  19901  dprdres  19960  dmdprdsplit2lem  19977  ringn0  20220  isdrng2  20652  drngmclOLD  20660  drngid2  20661  cnfldplusf  21308  cnfldsub  21309  cnsubmlem  21331  cnsubglem  21332  cnmsubglem  21347  gzrngunitlem  21349  rge0srg  21355  zring0  21368  pzriprnglem10  21400  zzngim  21462  zrhpsgnmhm  21493  re0g  21521  pjfval  21615  pjpm  21617  psrplusg  21845  coe1sfi  22098  ply1plusgfvi  22126  marep01ma  22547  smadiadetlem1a  22550  smadiadetlem3lem2  22554  smadiadetlem3  22555  smadiadetlem4  22556  smadiadet  22557  indistpsALT  22900  tgrest  23046  leordtval2  23099  lmbr2  23146  cnprest  23176  lmff  23188  kgenidm  23434  tx1cn  23496  tx2cn  23497  ustbas  24115  psmetge0  24200  xmetge0  24232  qdensere  24657  cnblcld  24662  cnfldms  24663  cnfldtopn  24669  xrsdsre  24699  xrge0tsms  24723  iccpnfcnv  24842  xrhmeo  24844  cnheiborlem  24853  cnlmod  25040  recvs  25046  lmmbr2  25159  lmcau  25213  metsscmetcld  25215  cncms  25255  cnfldcusp  25257  ovolctb  25391  ovoliunnul  25408  ismbl  25427  volf  25430  voliunlem1  25451  ioorf  25474  ioorinv  25477  ioorcl  25478  dyaddisj  25497  dyadmax  25499  dyadmbl  25501  mbfid  25536  ismbfd  25540  mbfimaopnlem  25556  limcresi  25786  dvreslem  25810  dvres2lem  25811  dvcjbr  25853  dvferm1  25889  dvferm2  25891  dvlip2  25900  dv11cn  25906  deg1ldg  25997  deg1leb  26000  plycpn  26197  vieta1lem2  26219  elqaa  26230  aalioulem2  26241  aaliou3lem3  26252  aaliou3lem4  26254  pserulm  26331  psercnlem2  26334  psercnlem1  26335  psercn  26336  abelth  26351  reeff1o  26357  pilem1  26361  efhalfpi  26380  coseq0negpitopi  26412  pige3ALT  26429  tanregt0  26448  efif1olem3  26453  efif1olem4  26454  efifo  26456  eff1olem  26457  efsubm  26460  logrn  26467  ellogrn  26468  relogf1o  26475  argregt0  26519  argrege0  26520  dvrelog  26546  dvloglem  26557  logf1o2  26559  dvlog  26560  efopnlem1  26565  efopnlem2  26566  logtayl  26569  cxpcn3lem  26657  cxpcn3  26658  resqrtcn  26659  asinneg  26796  asinrebnd  26811  atan0  26818  atanbnd  26836  areambl  26868  sqrtlim  26883  amgmlem  26900  lgamucov  26948  basellem1  26991  basellem4  26994  sqff1o  27092  dchrplusg  27158  bposlem6  27200  bposlem8  27202  dchrvmasumlem2  27409  pntibndlem1  27500  pntlemo  27518  qrng0  27532  ostth  27550  noextendseq  27579  bday0s  27740  oldlim  27798  zsex  28268  lmif  28712  islmib  28714  structiedg0val  28949  snstriedgval  28965  umgredgnlp  29074  usgrexmplef  29186  usgrexmpledg  29189  vtxdlfgrval  29413  upgr2pthnlp  29662  konigsberglem5  30185  ex-mod  30378  pliguhgr  30415  grporn  30450  ip0i  30754  ubthlem1  30799  ubthlem2  30800  axhcompl-zf  30927  normlem7  31045  bcseqi  31049  bcsiALT  31108  hlimf  31166  hlimuni  31167  hhssabloilem  31190  hhshsslem1  31196  hhsssh  31198  hhsscms  31207  occllem  31232  occl  31233  h1deoi  31478  h1dei  31479  h1de2ctlem  31484  h1de2ci  31485  spansni  31486  spanunsni  31508  pjpythi  31651  nmfn0  31916  nmopadjlem  32018  adjcoi  32029  nmopcoadji  32030  pjoccoi  32107  shatomistici  32290  iuninc  32489  imadifxp  32530  xppreima  32569  1stpreima  32630  2ndpreima  32631  fsuppcurry1  32648  fsuppcurry2  32649  hashgt1  32733  s3clhash  32869  gsummpt2d  32989  xrge0tsmsd  33002  tocyc01  33075  cyc3evpm  33107  cycpmconjslem2  33112  cyc3conja  33114  reofld  33315  rearchi  33317  nn0archi  33318  xrge0slmod  33319  elrspunidl  33399  dimval  33596  dimvalfi  33597  ply1degltdimlem  33618  algextdeglem8  33714  qtophaus  33826  iistmd  33892  xpinpreima  33896  xpinpreima2  33897  tpr2rico  33902  mndpluscn  33916  xrge0pluscn  33930  cnzh  33958  rezh  33959  qqhucn  33982  rrhcn  33987  cnrrext  34000  zrhre  34009  qqhre  34010  ismntop  34016  sigaex  34100  brsiga  34173  cntnevol  34218  voliune  34219  ddemeas  34226  1stmbfm  34251  2ndmbfm  34252  br2base  34260  dya2icoseg2  34269  dya2iocucvr  34275  carsgclctunlem2  34310  carsgclctunlem3  34311  sitgaddlemb  34339  eulerpartlemt  34362  eulerpartgbij  34363  eulerpartlemmf  34366  eulerpartlemgvv  34367  eulerpartlemgf  34370  eulerpart  34373  sseqmw  34382  sseqf  34383  sseqp1  34386  fiblem  34389  fibp1  34392  dstrvprob  34463  coinflipspace  34472  coinfliprv  34474  coinflippv  34475  ballotlem1  34478  ballotlem8  34528  circlemethhgt  34634  onvf1od  35094  usgrcyclgt2v  35118  iccllysconn  35237  rellysconn  35238  satf00  35361  fmla0  35369  msrid  35532  dfrdg2  35783  dfrdg4  35939  imagesset  35941  elhf  36162  filnetlem3  36368  limsucncmpi  36433  bj-babygodel  36591  bj-idres  37148  taupilem3  37307  icoreresf  37340  icoreelrnab  37342  relowlssretop  37351  poimirlem3  37617  poimirlem9  37623  poimirlem15  37629  poimirlem16  37630  poimirlem17  37631  poimirlem19  37633  poimirlem27  37641  poimirlem28  37642  poimirlem31  37645  poimirlem32  37646  mblfinlem1  37651  ovoliunnfl  37656  voliunnfl  37658  mbfresfi  37660  dvtan  37664  itg2addnc  37668  ftc1anclem3  37689  areacirc  37707  fdc  37739  ismrer1  37832  reheibor  37833  rngomndo  37929  gidsn  37946  ac6s6f  38167  cnvref4  38332  dfcnvrefrels2  38519  dfcnvrefrels3  38520  dedths  38955  tendo0co2  40782  erng1r  40989  dvalveclem  41019  dva0g  41021  dvh0g  41105  sn-it0e0  42404  sn-0tie0  42439  2rexfrabdioph  42784  3rexfrabdioph  42785  4rexfrabdioph  42786  6rexfrabdioph  42787  7rexfrabdioph  42788  rencldnfi  42809  jm2.27dlem2  42999  wepwso  43032  dfac11  43051  pwssplit4  43078  frlmpwfi  43087  isnumbasgrplem3  43094  mpaaeu  43139  proot1mul  43183  proot1hash  43184  epirron  43243  oneptr  43244  ordeldif1o  43249  oaomoencom  43306  oenassex  43307  cnvcnvintabd  43589  cnvrcl0  43614  dfrtrcl5  43618  cotrcltrcl  43714  frege92  43944  seff  44298  prmunb2  44300  binomcxplemdvbinom  44342  binomcxplemcvg  44343  binomcxplemnotnn0  44345  permac8prim  45004  sumsnd  45020  islptre  45617  stoweidlem34  46032  stoweidlem37  46035  stirlinglem11  46082  stirlinglem12  46083  stirlinglem13  46084  fouriersw  46229  natlocalincr  46874  upwordsing  46882  fundcmpsurbijinjpreimafv  47408  fundcmpsurinjimaid  47412  fmtnoinf  47537  gbowge7  47764  nnsum3primes4  47789  usgrexmpl12ngrlic  48030  gpgprismgr4cycllem2  48086  gpg5ngric  48118  2zrng0  48232  lmodn0  48484  zlmodzxzldeplem3  48491  lvecpsslmod  48496  0dig2pr01  48599  nelsubc3lem  49059  aacllem  49790  amgmwlem  49791