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  1616  ceqsexv2dOLD  3518  dtruALT2  5370  dtruOLD  5443  intasym  6122  relcoi2  6283  funres11  6631  cnvresid  6633  omsindsOLD  7893  find  7903  fparlem1  8117  fparlem2  8118  dftpos4  8251  tposf12  8257  wfrlem14OLD  8343  tfr2b  8417  tz7.44lem1  8426  ord3  8504  xp01disjl  8513  on2recsfn  8688  on2recsov  8689  on2ind  8690  on3ind  8691  xpcomco  9087  sbthlem2  9109  fidomdm  9355  brwdom2  9598  epnsym  9634  inf3lem6  9658  omex  9668  cnfcom  9725  ttrclco  9743  ttrclselem2  9751  tz9.1c  9755  frr1  9784  r1tr  9801  r1ord3g  9804  rankwflemb  9818  r1elwf  9821  r1elss  9831  rankval3b  9851  onssr1  9856  inlresf  9939  inrresf  9941  djuin  9943  infxpenlem  10038  alephnbtwn  10096  alephordilem1  10098  alephfp  10133  dfac13  10167  pwsdompw  10229  infdjuabs  10231  ackbij1  10263  ackbij2  10268  r1om  10269  cflim2  10288  fin23lem27  10353  fin23lem29  10366  fin23lem30  10367  fin1a2lem6  10430  fin1a2lem7  10431  fin1a2lem13  10437  itunitc1  10445  itunitc  10446  ituniiun  10447  hsmexlem5  10455  axcc2lem  10461  axcc3  10463  zorn2lem6  10526  zorn2lem7  10527  ttukeylem6  10539  axdc  10546  dmct  10549  iunfo  10564  cardval  10571  cardid  10572  pwcfsdom  10608  alephom  10610  canthp1lem2  10678  gchaleph2  10697  r1limwun  10761  inaprc  10861  nqerf  10955  recmulnq  10989  dmrecnq  10993  halfnq  11001  genpdm  11027  reclem3pr  11074  axresscn  11173  axpre-sup  11194  1re  11246  0re  11248  00id  11421  addrid  11426  0cnALT  11480  renegcli  11553  zexALT  12611  uzn0  12872  xrinfmss  13324  axdc4uzlem  13984  facnn  14270  fac0  14271  hashgval  14328  hashinf  14330  hashresfn  14335  hashrabrsn  14367  hashrabsn01  14368  hashrabsn1  14369  hashp1i  14398  hash1snb  14414  hashxplem  14428  fi1uzind  14494  cshw1  14808  cats1fv  14846  trclubgi  14980  cnrecnv  15148  rexanuz  15328  climdm  15534  lo1eq  15548  rlimeq  15549  sumsnf  15725  tanval  16108  rpnnen2lem11  16204  rpnnen  16207  sadadd2lem  16437  sadadd3  16439  sadaddlem  16444  sadasslem  16448  sadeq  16450  lcmgcdlem  16580  unbenlem  16880  prmreclem6  16893  vdwlem8  16960  vdwnnlem1  16967  0ram  16992  structcnvcnv  17125  prdsvallem  17439  prdsval  17440  prdsbas  17442  prdsplusg  17443  prdsmulr  17444  prdsvsca  17445  prdshom  17452  xpsfrn  17553  xpsff1o2  17554  catcoppccl  18109  catcoppcclOLD  18110  catcfuccl  18111  catcfucclOLD  18112  catcxpccl  18201  catcxpcclOLD  18202  tsrss  18584  gsumpropd2lem  18642  smndex2dnrinv  18875  mvdco  19412  efgmnvl  19681  efgval  19684  efgi0  19687  efgi1  19688  efgredeu  19719  0frgp  19746  abln0  19834  lt6abl  19862  gsumval3  19874  gsum2dlem2  19938  dprdres  19997  dmdprdsplit2lem  20014  ringn0  20259  isdrng2  20650  drngmcl  20653  drngid2  20657  cnfldplusf  21341  cnfldsub  21342  cnsubmlem  21364  cnsubglem  21365  cnmsubglem  21380  gzrngunitlem  21382  rge0srg  21388  zring0  21401  pzriprnglem10  21433  zzngim  21503  zrhpsgnmhm  21533  re0g  21561  pjfval  21657  pjpm  21659  psrplusg  21898  coe1sfi  22156  ply1plusgfvi  22184  marep01ma  22606  smadiadetlem1a  22609  smadiadetlem3lem2  22613  smadiadetlem3  22614  smadiadetlem4  22615  smadiadet  22616  indistpsALT  22960  indistpsALTOLD  22961  tgrest  23107  leordtval2  23160  lmbr2  23207  cnprest  23237  lmff  23249  kgenidm  23495  tx1cn  23557  tx2cn  23558  ustbas  24176  psmetge0  24262  xmetge0  24294  qdensere  24730  cnblcld  24735  cnfldms  24736  cnfldtopn  24742  xrsdsre  24770  xrge0tsms  24794  iccpnfcnv  24913  xrhmeo  24915  cnheiborlem  24924  cnlmod  25111  recvs  25117  lmmbr2  25231  lmcau  25285  metsscmetcld  25287  cncms  25327  cnfldcusp  25329  ovolctb  25463  ovoliunnul  25480  ismbl  25499  volf  25502  voliunlem1  25523  ioorf  25546  ioorinv  25549  ioorcl  25550  dyaddisj  25569  dyadmax  25571  dyadmbl  25573  mbfid  25608  ismbfd  25612  mbfimaopnlem  25628  limcresi  25858  dvreslem  25882  dvres2lem  25883  dvcjbr  25925  dvferm1  25961  dvferm2  25963  dvlip2  25972  dv11cn  25978  deg1ldg  26072  deg1leb  26075  plycpn  26269  vieta1lem2  26291  elqaa  26302  aalioulem2  26313  aaliou3lem3  26324  aaliou3lem4  26326  pserulm  26403  psercnlem2  26406  psercnlem1  26407  psercn  26408  abelth  26423  reeff1o  26429  pilem1  26433  efhalfpi  26451  coseq0negpitopi  26483  pige3ALT  26499  tanregt0  26518  efif1olem3  26523  efif1olem4  26524  efifo  26526  eff1olem  26527  efsubm  26530  logrn  26537  ellogrn  26538  relogf1o  26545  argregt0  26589  argrege0  26590  dvrelog  26616  dvloglem  26627  logf1o2  26629  dvlog  26630  efopnlem1  26635  efopnlem2  26636  logtayl  26639  cxpcn3lem  26727  cxpcn3  26728  resqrtcn  26729  asinneg  26863  asinrebnd  26878  atan0  26885  atanbnd  26903  areambl  26935  sqrtlim  26950  amgmlem  26967  lgamucov  27015  basellem1  27058  basellem4  27061  sqff1o  27159  dchrplusg  27225  bposlem6  27267  bposlem8  27269  dchrvmasumlem2  27476  mulog2sum  27515  pntibndlem1  27567  pntlemo  27585  qrng0  27599  ostth  27617  noextendseq  27646  bday0s  27807  oldlim  27859  zsex  28279  lmif  28661  islmib  28663  structiedg0val  28907  snstriedgval  28923  umgredgnlp  29032  usgrexmplef  29144  usgrexmpledg  29147  vtxdlfgrval  29371  upgr2pthnlp  29618  konigsberglem5  30138  ex-mod  30331  pliguhgr  30368  grporn  30403  ip0i  30707  ubthlem1  30752  ubthlem2  30753  axhcompl-zf  30880  normlem7  30998  bcseqi  31002  bcsiALT  31061  hlimf  31119  hlimuni  31120  hhssabloilem  31143  hhshsslem1  31149  hhsssh  31151  hhsscms  31160  occllem  31185  occl  31186  h1deoi  31431  h1dei  31432  h1de2ctlem  31437  h1de2ci  31438  spansni  31439  spanunsni  31461  pjpythi  31604  nmfn0  31869  nmopadjlem  31971  adjcoi  31982  nmopcoadji  31983  pjoccoi  32060  shatomistici  32243  iuninc  32430  imadifxp  32470  xppreima  32513  1stpreima  32568  2ndpreima  32569  fsuppcurry1  32589  fsuppcurry2  32590  hashgt1  32660  s3clhash  32758  gsummpt2d  32853  xrge0tsmsd  32861  tocyc01  32931  cyc3evpm  32963  cycpmconjslem2  32968  cyc3conja  32970  reofld  33155  rearchi  33157  nn0archi  33158  xrge0slmod  33159  elrspunidl  33240  dimval  33429  dimvalfi  33430  ply1degltdimlem  33451  algextdeglem8  33523  qtophaus  33568  iistmd  33634  xpinpreima  33638  xpinpreima2  33639  tpr2rico  33644  mndpluscn  33658  xrge0pluscn  33672  cnzh  33702  rezh  33703  qqhucn  33724  rrhcn  33729  cnrrext  33742  zrhre  33751  qqhre  33752  ismntop  33758  sigaex  33860  brsiga  33933  cntnevol  33978  voliune  33979  ddemeas  33986  1stmbfm  34011  2ndmbfm  34012  br2base  34020  dya2icoseg2  34029  dya2iocucvr  34035  carsgclctunlem2  34070  carsgclctunlem3  34071  sitgaddlemb  34099  eulerpartlemt  34122  eulerpartgbij  34123  eulerpartlemmf  34126  eulerpartlemgvv  34127  eulerpartlemgf  34130  eulerpart  34133  sseqmw  34142  sseqf  34143  sseqp1  34146  fiblem  34149  fibp1  34152  dstrvprob  34222  coinflipspace  34231  coinfliprv  34233  coinflippv  34234  ballotlem1  34237  ballotlem8  34287  circlemethhgt  34406  usgrcyclgt2v  34872  iccllysconn  34991  rellysconn  34992  satf00  35115  fmla0  35123  msrid  35286  dfrdg2  35522  dfrdg4  35678  imagesset  35680  elhf  35901  filnetlem3  35995  limsucncmpi  36060  bj-babygodel  36211  bj-idres  36770  taupilem3  36929  icoreresf  36962  icoreelrnab  36964  relowlssretop  36973  poimirlem3  37227  poimirlem9  37233  poimirlem15  37239  poimirlem16  37240  poimirlem17  37241  poimirlem19  37243  poimirlem27  37251  poimirlem28  37252  poimirlem31  37255  poimirlem32  37256  mblfinlem1  37261  ovoliunnfl  37266  voliunnfl  37268  mbfresfi  37270  dvtan  37274  itg2addnc  37278  ftc1anclem3  37299  areacirc  37317  fdc  37349  ismrer1  37442  reheibor  37443  rngomndo  37539  gidsn  37556  ac6s6f  37777  eccnvepex  37937  cnvref4  37952  dfcnvrefrels2  38130  dfcnvrefrels3  38131  dedths  38564  tendo0co2  40391  erng1r  40598  dvalveclem  40628  dva0g  40630  dvh0g  40714  sn-it0e0  42105  sn-0tie0  42129  2rexfrabdioph  42358  3rexfrabdioph  42359  4rexfrabdioph  42360  6rexfrabdioph  42361  7rexfrabdioph  42362  rencldnfi  42383  jm2.27dlem2  42573  wepwso  42609  dfac11  42628  pwssplit4  42655  frlmpwfi  42664  isnumbasgrplem3  42671  mpaaeu  42716  proot1mul  42764  proot1hash  42765  epirron  42824  oneptr  42825  ordeldif1o  42831  oaomoencom  42888  oenassex  42889  cnvcnvintabd  43172  cnvrcl0  43197  dfrtrcl5  43201  cotrcltrcl  43297  frege92  43527  seff  43888  prmunb2  43890  binomcxplemdvbinom  43932  binomcxplemcvg  43933  binomcxplemnotnn0  43935  sumsnd  44530  islptre  45145  stoweidlem34  45560  stoweidlem37  45563  stirlinglem11  45610  stirlinglem12  45611  stirlinglem13  45612  fouriersw  45757  natlocalincr  46400  upwordsing  46408  fundcmpsurbijinjpreimafv  46884  fundcmpsurinjimaid  46888  fmtnoinf  47013  gbowge7  47240  nnsum3primes4  47265  2zrng0  47492  lmodn0  47749  zlmodzxzldeplem3  47756  lvecpsslmod  47761  0dig2pr01  47869  aacllem  48420  amgmwlem  48421