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  3503  dtruALT2  5328  dtruOLD  5404  intasym  6091  relcoi2  6253  funres11  6596  cnvresid  6598  find  7874  fparlem1  8094  fparlem2  8095  dftpos4  8227  tposf12  8233  tfr2b  8367  tz7.44lem1  8376  ord3  8452  xp01disjl  8459  on2recsfn  8634  on2recsov  8635  on2ind  8636  on3ind  8637  xpcomco  9036  sbthlem2  9058  fidomdm  9292  brwdom2  9533  epnsym  9569  inf3lem6  9593  cnfcom  9660  ttrclco  9678  ttrclselem2  9686  tz9.1c  9690  frr1  9719  r1tr  9736  r1ord3g  9739  rankwflemb  9753  r1elwf  9756  r1elss  9766  rankval3b  9786  onssr1  9791  inlresf  9874  inrresf  9876  djuin  9878  infxpenlem  9973  alephnbtwn  10031  alephordilem1  10033  alephfp  10068  dfac13  10103  pwsdompw  10163  infdjuabs  10165  ackbij1  10197  ackbij2  10202  r1om  10203  cflim2  10223  fin23lem27  10288  fin23lem29  10301  fin23lem30  10302  fin1a2lem6  10365  fin1a2lem7  10366  fin1a2lem13  10372  itunitc1  10380  itunitc  10381  ituniiun  10382  hsmexlem5  10390  axcc2lem  10396  axcc3  10398  zorn2lem6  10461  zorn2lem7  10462  ttukeylem6  10474  dmct  10484  iunfo  10499  cardval  10506  cardid  10507  alephom  10545  canthp1lem2  10613  gchaleph2  10632  r1limwun  10696  inaprc  10796  nqerf  10890  recmulnq  10924  dmrecnq  10928  halfnq  10936  genpdm  10962  reclem3pr  11009  axresscn  11108  axpre-sup  11129  1re  11181  0re  11183  00id  11356  addrid  11361  0cnALT  11416  renegcli  11490  zexALT  12556  uzn0  12817  xrinfmss  13277  axdc4uzlem  13955  facnn  14247  fac0  14248  hashgval  14305  hashinf  14307  hashresfn  14312  hashrabrsn  14344  hashrabsn01  14345  hashrabsn1  14346  hashp1i  14375  hash1snb  14391  hashxplem  14405  fi1uzind  14479  cshw1  14794  cats1fv  14832  s7f1o  14939  trclubgi  14970  cnrecnv  15138  rexanuz  15319  climdm  15527  lo1eq  15541  rlimeq  15542  sumsnf  15716  tanval  16103  rpnnen2lem11  16199  rpnnen  16202  sadadd2lem  16436  sadadd3  16438  sadaddlem  16443  sadasslem  16447  sadeq  16449  lcmgcdlem  16583  unbenlem  16886  prmreclem6  16899  vdwlem8  16966  vdwnnlem1  16973  0ram  16998  structcnvcnv  17130  prdsvallem  17424  prdsval  17425  prdsbas  17427  prdsplusg  17428  prdsmulr  17429  prdsvsca  17430  prdshom  17437  xpsfrn  17538  xpsff1o2  17539  catcoppccl  18086  catcfuccl  18087  catcxpccl  18175  tsrss  18555  gsumpropd2lem  18613  smndex2dnrinv  18849  mvdco  19382  efgmnvl  19651  efgval  19654  efgi0  19657  efgi1  19658  efgredeu  19689  0frgp  19716  abln0  19804  lt6abl  19832  gsumval3  19844  gsum2dlem2  19908  dprdres  19967  dmdprdsplit2lem  19984  ringn0  20227  isdrng2  20659  drngmclOLD  20667  drngid2  20668  cnfldplusf  21315  cnfldsub  21316  cnsubmlem  21338  cnsubglem  21339  cnmsubglem  21354  gzrngunitlem  21356  rge0srg  21362  zring0  21375  pzriprnglem10  21407  zzngim  21469  zrhpsgnmhm  21500  re0g  21528  pjfval  21622  pjpm  21624  psrplusg  21852  coe1sfi  22105  ply1plusgfvi  22133  marep01ma  22554  smadiadetlem1a  22557  smadiadetlem3lem2  22561  smadiadetlem3  22562  smadiadetlem4  22563  smadiadet  22564  indistpsALT  22907  tgrest  23053  leordtval2  23106  lmbr2  23153  cnprest  23183  lmff  23195  kgenidm  23441  tx1cn  23503  tx2cn  23504  ustbas  24122  psmetge0  24207  xmetge0  24239  qdensere  24664  cnblcld  24669  cnfldms  24670  cnfldtopn  24676  xrsdsre  24706  xrge0tsms  24730  iccpnfcnv  24849  xrhmeo  24851  cnheiborlem  24860  cnlmod  25047  recvs  25053  lmmbr2  25166  lmcau  25220  metsscmetcld  25222  cncms  25262  cnfldcusp  25264  ovolctb  25398  ovoliunnul  25415  ismbl  25434  volf  25437  voliunlem1  25458  ioorf  25481  ioorinv  25484  ioorcl  25485  dyaddisj  25504  dyadmax  25506  dyadmbl  25508  mbfid  25543  ismbfd  25547  mbfimaopnlem  25563  limcresi  25793  dvreslem  25817  dvres2lem  25818  dvcjbr  25860  dvferm1  25896  dvferm2  25898  dvlip2  25907  dv11cn  25913  deg1ldg  26004  deg1leb  26007  plycpn  26204  vieta1lem2  26226  elqaa  26237  aalioulem2  26248  aaliou3lem3  26259  aaliou3lem4  26261  pserulm  26338  psercnlem2  26341  psercnlem1  26342  psercn  26343  abelth  26358  reeff1o  26364  pilem1  26368  efhalfpi  26387  coseq0negpitopi  26419  pige3ALT  26436  tanregt0  26455  efif1olem3  26460  efif1olem4  26461  efifo  26463  eff1olem  26464  efsubm  26467  logrn  26474  ellogrn  26475  relogf1o  26482  argregt0  26526  argrege0  26527  dvrelog  26553  dvloglem  26564  logf1o2  26566  dvlog  26567  efopnlem1  26572  efopnlem2  26573  logtayl  26576  cxpcn3lem  26664  cxpcn3  26665  resqrtcn  26666  asinneg  26803  asinrebnd  26818  atan0  26825  atanbnd  26843  areambl  26875  sqrtlim  26890  amgmlem  26907  lgamucov  26955  basellem1  26998  basellem4  27001  sqff1o  27099  dchrplusg  27165  bposlem6  27207  bposlem8  27209  dchrvmasumlem2  27416  pntibndlem1  27507  pntlemo  27525  qrng0  27539  ostth  27557  noextendseq  27586  bday0s  27747  oldlim  27805  zsex  28275  lmif  28719  islmib  28721  structiedg0val  28956  snstriedgval  28972  umgredgnlp  29081  usgrexmplef  29193  usgrexmpledg  29196  vtxdlfgrval  29420  upgr2pthnlp  29669  konigsberglem5  30192  ex-mod  30385  pliguhgr  30422  grporn  30457  ip0i  30761  ubthlem1  30806  ubthlem2  30807  axhcompl-zf  30934  normlem7  31052  bcseqi  31056  bcsiALT  31115  hlimf  31173  hlimuni  31174  hhssabloilem  31197  hhshsslem1  31203  hhsssh  31205  hhsscms  31214  occllem  31239  occl  31240  h1deoi  31485  h1dei  31486  h1de2ctlem  31491  h1de2ci  31492  spansni  31493  spanunsni  31515  pjpythi  31658  nmfn0  31923  nmopadjlem  32025  adjcoi  32036  nmopcoadji  32037  pjoccoi  32114  shatomistici  32297  iuninc  32496  imadifxp  32537  xppreima  32576  1stpreima  32637  2ndpreima  32638  fsuppcurry1  32655  fsuppcurry2  32656  hashgt1  32740  s3clhash  32876  gsummpt2d  32996  xrge0tsmsd  33009  tocyc01  33082  cyc3evpm  33114  cycpmconjslem2  33119  cyc3conja  33121  reofld  33322  rearchi  33324  nn0archi  33325  xrge0slmod  33326  elrspunidl  33406  dimval  33603  dimvalfi  33604  ply1degltdimlem  33625  algextdeglem8  33721  qtophaus  33833  iistmd  33899  xpinpreima  33903  xpinpreima2  33904  tpr2rico  33909  mndpluscn  33923  xrge0pluscn  33937  cnzh  33965  rezh  33966  qqhucn  33989  rrhcn  33994  cnrrext  34007  zrhre  34016  qqhre  34017  ismntop  34023  sigaex  34107  brsiga  34180  cntnevol  34225  voliune  34226  ddemeas  34233  1stmbfm  34258  2ndmbfm  34259  br2base  34267  dya2icoseg2  34276  dya2iocucvr  34282  carsgclctunlem2  34317  carsgclctunlem3  34318  sitgaddlemb  34346  eulerpartlemt  34369  eulerpartgbij  34370  eulerpartlemmf  34373  eulerpartlemgvv  34374  eulerpartlemgf  34377  eulerpart  34380  sseqmw  34389  sseqf  34390  sseqp1  34393  fiblem  34396  fibp1  34399  dstrvprob  34470  coinflipspace  34479  coinfliprv  34481  coinflippv  34482  ballotlem1  34485  ballotlem8  34535  circlemethhgt  34641  onvf1od  35101  usgrcyclgt2v  35125  iccllysconn  35244  rellysconn  35245  satf00  35368  fmla0  35376  msrid  35539  dfrdg2  35790  dfrdg4  35946  imagesset  35948  elhf  36169  filnetlem3  36375  limsucncmpi  36440  bj-babygodel  36598  bj-idres  37155  taupilem3  37314  icoreresf  37347  icoreelrnab  37349  relowlssretop  37358  poimirlem3  37624  poimirlem9  37630  poimirlem15  37636  poimirlem16  37637  poimirlem17  37638  poimirlem19  37640  poimirlem27  37648  poimirlem28  37649  poimirlem31  37652  poimirlem32  37653  mblfinlem1  37658  ovoliunnfl  37663  voliunnfl  37665  mbfresfi  37667  dvtan  37671  itg2addnc  37675  ftc1anclem3  37696  areacirc  37714  fdc  37746  ismrer1  37839  reheibor  37840  rngomndo  37936  gidsn  37953  ac6s6f  38174  cnvref4  38339  dfcnvrefrels2  38526  dfcnvrefrels3  38527  dedths  38962  tendo0co2  40789  erng1r  40996  dvalveclem  41026  dva0g  41028  dvh0g  41112  sn-it0e0  42411  sn-0tie0  42446  2rexfrabdioph  42791  3rexfrabdioph  42792  4rexfrabdioph  42793  6rexfrabdioph  42794  7rexfrabdioph  42795  rencldnfi  42816  jm2.27dlem2  43006  wepwso  43039  dfac11  43058  pwssplit4  43085  frlmpwfi  43094  isnumbasgrplem3  43101  mpaaeu  43146  proot1mul  43190  proot1hash  43191  epirron  43250  oneptr  43251  ordeldif1o  43256  oaomoencom  43313  oenassex  43314  cnvcnvintabd  43596  cnvrcl0  43621  dfrtrcl5  43625  cotrcltrcl  43721  frege92  43951  seff  44305  prmunb2  44307  binomcxplemdvbinom  44349  binomcxplemcvg  44350  binomcxplemnotnn0  44352  permac8prim  45011  sumsnd  45027  islptre  45624  stoweidlem34  46039  stoweidlem37  46042  stirlinglem11  46089  stirlinglem12  46090  stirlinglem13  46091  fouriersw  46236  natlocalincr  46881  upwordsing  46889  fundcmpsurbijinjpreimafv  47412  fundcmpsurinjimaid  47416  fmtnoinf  47541  gbowge7  47768  nnsum3primes4  47793  usgrexmpl12ngrlic  48034  gpgprismgr4cycllem2  48090  gpg5ngric  48122  2zrng0  48236  lmodn0  48488  zlmodzxzldeplem3  48495  lvecpsslmod  48500  0dig2pr01  48603  nelsubc3lem  49063  aacllem  49794  amgmwlem  49795