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  1624  nfcriOLD  2893  nfcriOLDOLD  2894  ceqsexv2d  3528  dtruALT2  5368  dtruOLD  5441  intasym  6116  relcoi2  6276  funres11  6625  cnvresid  6627  omsindsOLD  7879  find  7889  fparlem1  8100  fparlem2  8101  dftpos4  8232  tposf12  8238  wfrlem14OLD  8324  tfr2b  8398  tz7.44lem1  8407  ord3  8485  xp01disjl  8494  on2recsfn  8668  on2recsov  8669  on2ind  8670  on3ind  8671  xpcomco  9064  sbthlem2  9086  fidomdm  9331  brwdom2  9570  epnsym  9606  inf3lem6  9630  omex  9640  cnfcom  9697  ttrclco  9715  ttrclselem2  9723  tz9.1c  9727  frr1  9756  r1tr  9773  r1ord3g  9776  rankwflemb  9790  r1elwf  9793  r1elss  9803  rankval3b  9823  onssr1  9828  inlresf  9911  inrresf  9913  djuin  9915  infxpenlem  10010  alephnbtwn  10068  alephordilem1  10070  alephfp  10105  dfac13  10139  pwsdompw  10201  infdjuabs  10203  ackbij1  10235  ackbij2  10240  r1om  10241  cflim2  10260  fin23lem27  10325  fin23lem29  10338  fin23lem30  10339  fin1a2lem6  10402  fin1a2lem7  10403  fin1a2lem13  10409  itunitc1  10417  itunitc  10418  ituniiun  10419  hsmexlem5  10427  axcc2lem  10433  axcc3  10435  zorn2lem6  10498  zorn2lem7  10499  ttukeylem6  10511  axdc  10518  dmct  10521  iunfo  10536  cardval  10543  cardid  10544  pwcfsdom  10580  alephom  10582  canthp1lem2  10650  gchaleph2  10669  r1limwun  10733  inaprc  10833  nqerf  10927  recmulnq  10961  dmrecnq  10965  halfnq  10973  genpdm  10999  reclem3pr  11046  axresscn  11145  axpre-sup  11166  1re  11216  0re  11218  00id  11391  addrid  11396  0cnALT  11450  renegcli  11523  zexALT  12580  uzn0  12841  xrinfmss  13291  axdc4uzlem  13950  facnn  14237  fac0  14238  hashgval  14295  hashinf  14297  hashresfn  14302  hashrabrsn  14334  hashrabsn01  14335  hashrabsn1  14336  hashp1i  14365  hash1snb  14381  hashxplem  14395  fi1uzind  14460  cshw1  14774  cats1fv  14812  trclubgi  14946  cnrecnv  15114  rexanuz  15294  climdm  15500  lo1eq  15514  rlimeq  15515  sumsnf  15691  tanval  16073  rpnnen2lem11  16169  rpnnen  16172  sadadd2lem  16402  sadadd3  16404  sadaddlem  16409  sadasslem  16413  sadeq  16415  lcmgcdlem  16545  unbenlem  16843  prmreclem6  16856  vdwlem8  16923  vdwnnlem1  16930  0ram  16955  structcnvcnv  17088  prdsvallem  17402  prdsval  17403  prdsbas  17405  prdsplusg  17406  prdsmulr  17407  prdsvsca  17408  prdshom  17415  xpsfrn  17516  xpsff1o2  17517  catcoppccl  18069  catcoppcclOLD  18070  catcfuccl  18071  catcfucclOLD  18072  catcxpccl  18161  catcxpcclOLD  18162  tsrss  18544  gsumpropd2lem  18600  smndex2dnrinv  18798  mvdco  19315  efgmnvl  19584  efgval  19587  efgi0  19590  efgi1  19591  efgredeu  19622  0frgp  19649  abln0  19737  lt6abl  19765  gsumval3  19777  gsum2dlem2  19841  dprdres  19900  dmdprdsplit2lem  19917  ringn0  20127  isdrng2  20375  drngmcl  20378  drngid2  20382  cnfldplusf  20978  cnfldsub  20979  cnsubmlem  20999  cnsubglem  21000  cnmsubglem  21014  gzrngunitlem  21016  rge0srg  21022  zring0  21034  zzngim  21114  zrhpsgnmhm  21143  re0g  21171  pjfval  21267  pjpm  21269  psrplusg  21506  coe1sfi  21743  ply1plusgfvi  21771  marep01ma  22169  smadiadetlem1a  22172  smadiadetlem3lem2  22176  smadiadetlem3  22177  smadiadetlem4  22178  smadiadet  22179  indistpsALT  22523  indistpsALTOLD  22524  tgrest  22670  leordtval2  22723  lmbr2  22770  cnprest  22800  lmff  22812  kgenidm  23058  tx1cn  23120  tx2cn  23121  ustbas  23739  psmetge0  23825  xmetge0  23857  qdensere  24293  cnblcld  24298  cnfldms  24299  cnfldtopn  24305  xrsdsre  24333  xrge0tsms  24357  iccpnfcnv  24467  xrhmeo  24469  cnheiborlem  24477  cnlmod  24663  recvs  24669  lmmbr2  24783  lmcau  24837  metsscmetcld  24839  cncms  24879  cnfldcusp  24881  ovolctb  25014  ovoliunnul  25031  ismbl  25050  volf  25053  voliunlem1  25074  ioorf  25097  ioorinv  25100  ioorcl  25101  dyaddisj  25120  dyadmax  25122  dyadmbl  25124  mbfid  25159  ismbfd  25163  mbfimaopnlem  25179  limcresi  25409  dvreslem  25433  dvres2lem  25434  dvcjbr  25473  dvferm1  25509  dvferm2  25511  dvlip2  25519  dv11cn  25525  deg1ldg  25617  deg1leb  25620  plycpn  25809  vieta1lem2  25831  elqaa  25842  aalioulem2  25853  aaliou3lem3  25864  aaliou3lem4  25866  pserulm  25941  psercnlem2  25943  psercnlem1  25944  psercn  25945  abelth  25960  reeff1o  25966  pilem1  25970  efhalfpi  25988  coseq0negpitopi  26020  pige3ALT  26036  tanregt0  26055  efif1olem3  26060  efif1olem4  26061  efifo  26063  eff1olem  26064  efsubm  26067  logrn  26074  ellogrn  26075  relogf1o  26082  argregt0  26125  argrege0  26126  dvrelog  26152  dvloglem  26163  logf1o2  26165  dvlog  26166  efopnlem1  26171  efopnlem2  26172  logtayl  26175  cxpcn3lem  26262  cxpcn3  26263  resqrtcn  26264  asinneg  26398  asinrebnd  26413  atan0  26420  atanbnd  26438  areambl  26470  sqrtlim  26484  amgmlem  26501  lgamucov  26549  basellem1  26592  basellem4  26595  sqff1o  26693  dchrplusg  26757  bposlem6  26799  bposlem8  26801  dchrvmasumlem2  27008  mulog2sum  27047  pntibndlem1  27099  pntlemo  27117  qrng0  27131  ostth  27149  noextendseq  27177  bday0s  27337  oldlim  27389  lmif  28074  islmib  28076  structiedg0val  28320  snstriedgval  28336  umgredgnlp  28445  usgrexmplef  28554  usgrexmpledg  28557  vtxdlfgrval  28780  upgr2pthnlp  29027  konigsberglem5  29547  ex-mod  29740  pliguhgr  29777  grporn  29812  ip0i  30116  ubthlem1  30161  ubthlem2  30162  axhcompl-zf  30289  normlem7  30407  bcseqi  30411  bcsiALT  30470  hlimf  30528  hlimuni  30529  hhssabloilem  30552  hhshsslem1  30558  hhsssh  30560  hhsscms  30569  occllem  30594  occl  30595  h1deoi  30840  h1dei  30841  h1de2ctlem  30846  h1de2ci  30847  spansni  30848  spanunsni  30870  pjpythi  31013  nmfn0  31278  nmopadjlem  31380  adjcoi  31391  nmopcoadji  31392  pjoccoi  31469  shatomistici  31652  iuninc  31830  imadifxp  31870  xppreima  31909  1stpreima  31966  2ndpreima  31967  fsuppcurry1  31988  fsuppcurry2  31989  hashgt1  32058  s3clhash  32152  gsummpt2d  32242  xrge0tsmsd  32250  tocyc01  32318  cyc3evpm  32350  cycpmconjslem2  32355  cyc3conja  32357  reofld  32500  rearchi  32502  nn0archi  32503  xrge0slmod  32504  elrspunidl  32591  dimval  32744  dimvalfi  32745  ply1degltdimlem  32766  algextdeglem8  32840  qtophaus  32885  iistmd  32951  xpinpreima  32955  xpinpreima2  32956  tpr2rico  32961  mndpluscn  32975  xrge0pluscn  32989  cnzh  33019  rezh  33020  qqhucn  33041  rrhcn  33046  cnrrext  33059  zrhre  33068  qqhre  33069  ismntop  33075  sigaex  33177  brsiga  33250  cntnevol  33295  voliune  33296  ddemeas  33303  1stmbfm  33328  2ndmbfm  33329  br2base  33337  dya2icoseg2  33346  dya2iocucvr  33352  carsgclctunlem2  33387  carsgclctunlem3  33388  sitgaddlemb  33416  eulerpartlemt  33439  eulerpartgbij  33440  eulerpartlemmf  33443  eulerpartlemgvv  33444  eulerpartlemgf  33447  eulerpart  33450  sseqmw  33459  sseqf  33460  sseqp1  33463  fiblem  33466  fibp1  33469  dstrvprob  33539  coinflipspace  33548  coinfliprv  33550  coinflippv  33551  ballotlem1  33554  ballotlem8  33604  circlemethhgt  33724  usgrcyclgt2v  34191  iccllysconn  34310  rellysconn  34311  satf00  34434  fmla0  34442  msrid  34605  dfrdg2  34842  dfrdg4  34998  imagesset  35000  elhf  35221  filnetlem3  35357  limsucncmpi  35422  bj-babygodel  35573  bj-idres  36133  taupilem3  36292  icoreresf  36325  icoreelrnab  36327  relowlssretop  36336  poimirlem3  36583  poimirlem9  36589  poimirlem15  36595  poimirlem16  36596  poimirlem17  36597  poimirlem19  36599  poimirlem27  36607  poimirlem28  36608  poimirlem31  36611  poimirlem32  36612  mblfinlem1  36617  ovoliunnfl  36622  voliunnfl  36624  mbfresfi  36626  dvtan  36630  itg2addnc  36634  ftc1anclem3  36655  areacirc  36673  fdc  36705  ismrer1  36798  reheibor  36799  rngomndo  36895  gidsn  36912  ac6s6f  37133  eccnvepex  37296  cnvref4  37311  dfcnvrefrels2  37490  dfcnvrefrels3  37491  dedths  37924  tendo0co2  39751  erng1r  39958  dvalveclem  39988  dva0g  39990  dvh0g  40074  sn-it0e0  41376  sn-0tie0  41400  2rexfrabdioph  41622  3rexfrabdioph  41623  4rexfrabdioph  41624  6rexfrabdioph  41625  7rexfrabdioph  41626  rencldnfi  41647  jm2.27dlem2  41837  wepwso  41873  dfac11  41892  pwssplit4  41919  frlmpwfi  41928  isnumbasgrplem3  41935  mpaaeu  41980  proot1mul  42029  proot1hash  42030  epirron  42091  oneptr  42092  ordeldif1o  42098  oaomoencom  42155  oenassex  42156  cnvcnvintabd  42439  cnvrcl0  42464  dfrtrcl5  42468  cotrcltrcl  42564  frege92  42794  seff  43156  prmunb2  43158  binomcxplemdvbinom  43200  binomcxplemcvg  43201  binomcxplemnotnn0  43203  sumsnd  43798  islptre  44420  stoweidlem34  44835  stoweidlem37  44838  stirlinglem11  44885  stirlinglem12  44886  stirlinglem13  44887  fouriersw  45032  natlocalincr  45675  upwordsing  45683  fundcmpsurbijinjpreimafv  46160  fundcmpsurinjimaid  46164  fmtnoinf  46289  gbowge7  46516  nnsum3primes4  46541  pzriprnglem10  46899  2zrng0  46921  lmodn0  47260  zlmodzxzldeplem3  47267  lvecpsslmod  47272  0dig2pr01  47380  aacllem  47932  amgmwlem  47933