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  ceqsexv2dOLD  3481  dtruALT2  5307  intasym  6072  relcoi2  6235  funres11  6569  cnvresid  6571  find  7839  fparlem1  8055  fparlem2  8056  dftpos4  8188  tposf12  8194  tfr2b  8328  tz7.44lem1  8337  ord3  8413  xp01disjl  8420  on2recsfn  8596  on2recsov  8597  on2ind  8598  on3ind  8599  xpcomco  8998  sbthlem2  9019  fidomdm  9237  brwdom2  9481  epnsym  9521  inf3lem6  9545  cnfcom  9612  ttrclco  9630  ttrclselem2  9638  tz9.1c  9642  frr1  9674  r1tr  9691  r1ord3g  9694  rankwflemb  9708  r1elwf  9711  r1elss  9721  rankval3b  9741  onssr1  9746  inlresf  9829  inrresf  9831  djuin  9833  infxpenlem  9926  alephnbtwn  9984  alephordilem1  9986  alephfp  10021  dfac13  10056  pwsdompw  10116  infdjuabs  10118  ackbij1  10150  ackbij2  10155  r1om  10156  cflim2  10176  fin23lem27  10241  fin23lem29  10254  fin23lem30  10255  fin1a2lem6  10318  fin1a2lem7  10319  fin1a2lem13  10325  itunitc1  10333  itunitc  10334  ituniiun  10335  hsmexlem5  10343  axcc2lem  10349  axcc3  10351  zorn2lem6  10414  zorn2lem7  10415  ttukeylem6  10427  dmct  10437  iunfo  10452  cardval  10459  cardid  10460  alephom  10499  canthp1lem2  10567  gchaleph2  10586  r1limwun  10650  inaprc  10750  nqerf  10844  recmulnq  10878  dmrecnq  10882  halfnq  10890  genpdm  10916  reclem3pr  10963  axresscn  11062  axpre-sup  11083  1re  11135  0re  11137  00id  11312  addrid  11317  0cnALT  11372  renegcli  11446  zexALT  12535  uzn0  12796  xrinfmss  13253  axdc4uzlem  13936  facnn  14228  fac0  14229  hashgval  14286  hashinf  14288  hashresfn  14293  hashrabrsn  14325  hashrabsn01  14326  hashrabsn1  14327  hashp1i  14356  hash1snb  14372  hashxplem  14386  fi1uzind  14460  cshw1  14775  cats1fv  14812  s7f1o  14919  trclubgi  14950  cnrecnv  15118  rexanuz  15299  climdm  15507  lo1eq  15521  rlimeq  15522  sumsnf  15696  tanval  16086  rpnnen2lem11  16182  rpnnen  16185  sadadd2lem  16419  sadadd3  16421  sadaddlem  16426  sadasslem  16430  sadeq  16432  lcmgcdlem  16566  unbenlem  16870  prmreclem6  16883  vdwlem8  16950  vdwnnlem1  16957  0ram  16982  structcnvcnv  17114  prdsvallem  17408  prdsval  17409  prdsbas  17411  prdsplusg  17412  prdsmulr  17413  prdsvsca  17414  prdshom  17421  xpsfrn  17523  xpsff1o2  17524  catcoppccl  18075  catcfuccl  18076  catcxpccl  18164  tsrss  18546  gsumpropd2lem  18638  smndex2dnrinv  18877  mvdco  19411  efgmnvl  19680  efgval  19683  efgi0  19686  efgi1  19687  efgredeu  19718  0frgp  19745  abln0  19833  lt6abl  19861  gsumval3  19873  gsum2dlem2  19937  dprdres  19996  dmdprdsplit2lem  20013  ringn0  20283  isdrng2  20711  drngmclOLD  20719  drngid2  20720  cnfldplusf  21386  cnfldsub  21387  cnsubmlem  21404  cnsubglem  21405  cnmsubglem  21420  gzrngunitlem  21422  rge0srg  21428  zring0  21448  pzriprnglem10  21480  zzngim  21542  zrhpsgnmhm  21574  re0g  21602  pjfval  21696  pjpm  21698  psrplusg  21926  coe1sfi  22187  ply1plusgfvi  22215  marep01ma  22635  smadiadetlem1a  22638  smadiadetlem3lem2  22642  smadiadetlem3  22643  smadiadetlem4  22644  smadiadet  22645  indistpsALT  22988  tgrest  23134  leordtval2  23187  lmbr2  23234  cnprest  23264  lmff  23276  kgenidm  23522  tx1cn  23584  tx2cn  23585  ustbas  24202  psmetge0  24287  xmetge0  24319  qdensere  24744  cnblcld  24749  cnfldms  24750  cnfldtopn  24756  xrsdsre  24786  xrge0tsms  24810  iccpnfcnv  24921  xrhmeo  24923  cnheiborlem  24931  cnlmod  25117  recvs  25123  lmmbr2  25236  lmcau  25290  metsscmetcld  25292  cncms  25332  cnfldcusp  25334  ovolctb  25467  ovoliunnul  25484  ismbl  25503  volf  25506  voliunlem1  25527  ioorf  25550  ioorinv  25553  ioorcl  25554  dyaddisj  25573  dyadmax  25575  dyadmbl  25577  mbfid  25612  ismbfd  25616  mbfimaopnlem  25632  limcresi  25862  dvreslem  25886  dvres2lem  25887  dvcjbr  25926  dvferm1  25962  dvferm2  25964  dvlip2  25972  dv11cn  25978  deg1ldg  26067  deg1leb  26070  plycpn  26266  vieta1lem2  26288  elqaa  26299  aalioulem2  26310  aaliou3lem3  26321  aaliou3lem4  26323  pserulm  26400  psercnlem2  26402  psercnlem1  26403  psercn  26404  abelth  26419  reeff1o  26425  pilem1  26429  efhalfpi  26448  coseq0negpitopi  26480  pige3ALT  26497  tanregt0  26516  efif1olem3  26521  efif1olem4  26522  efifo  26524  eff1olem  26525  efsubm  26528  logrn  26535  ellogrn  26536  relogf1o  26543  argregt0  26587  argrege0  26588  dvrelog  26614  dvloglem  26625  logf1o2  26627  dvlog  26628  efopnlem1  26633  efopnlem2  26634  logtayl  26637  cxpcn3lem  26724  cxpcn3  26725  resqrtcn  26726  asinneg  26863  asinrebnd  26878  atan0  26885  atanbnd  26903  areambl  26935  sqrtlim  26950  amgmlem  26967  lgamucov  27015  basellem1  27058  basellem4  27061  sqff1o  27159  dchrplusg  27224  bposlem6  27266  bposlem8  27268  dchrvmasumlem2  27475  pntibndlem1  27566  pntlemo  27584  qrng0  27598  ostth  27616  noextendseq  27645  bday0  27817  oldlim  27893  ons2ind  28281  zsex  28386  lmif  28867  islmib  28869  structiedg0val  29105  snstriedgval  29121  umgredgnlp  29230  usgrexmplef  29342  usgrexmpledg  29345  vtxdlfgrval  29569  upgr2pthnlp  29815  konigsberglem5  30341  ex-mod  30534  nowisdomv  30559  pliguhgr  30572  grporn  30607  ip0i  30911  ubthlem1  30956  ubthlem2  30957  axhcompl-zf  31084  normlem7  31202  bcseqi  31206  bcsiALT  31265  hlimf  31323  hlimuni  31324  hhssabloilem  31347  hhshsslem1  31353  hhsssh  31355  hhsscms  31364  occllem  31389  occl  31390  h1deoi  31635  h1dei  31636  h1de2ctlem  31641  h1de2ci  31642  spansni  31643  spanunsni  31665  pjpythi  31808  nmfn0  32073  nmopadjlem  32175  adjcoi  32186  nmopcoadji  32187  pjoccoi  32264  shatomistici  32447  iuninc  32645  imadifxp  32686  xppreima  32733  1stpreima  32795  2ndpreima  32796  fsuppcurry1  32812  fsuppcurry2  32813  hashgt1  32896  s3clhash  33023  gsummpt2d  33125  xrge0tsmsd  33149  tocyc01  33194  cyc3evpm  33226  cycpmconjslem2  33231  cyc3conja  33233  reofld  33418  rearchi  33421  nn0archi  33422  xrge0slmod  33423  elrspunidl  33503  dimval  33760  dimvalfi  33761  ply1degltdimlem  33782  algextdeglem8  33884  qtophaus  33996  iistmd  34062  xpinpreima  34066  xpinpreima2  34067  tpr2rico  34072  mndpluscn  34086  xrge0pluscn  34100  cnzh  34128  rezh  34129  qqhucn  34152  rrhcn  34157  cnrrext  34170  zrhre  34179  qqhre  34180  ismntop  34186  sigaex  34270  brsiga  34343  cntnevol  34388  voliune  34389  ddemeas  34396  1stmbfm  34420  2ndmbfm  34421  br2base  34429  dya2icoseg2  34438  dya2iocucvr  34444  carsgclctunlem2  34479  carsgclctunlem3  34480  sitgaddlemb  34508  eulerpartlemt  34531  eulerpartgbij  34532  eulerpartlemmf  34535  eulerpartlemgvv  34536  eulerpartlemgf  34539  eulerpart  34542  sseqmw  34551  sseqf  34552  sseqp1  34555  fiblem  34558  fibp1  34561  dstrvprob  34632  coinflipspace  34641  coinfliprv  34643  coinflippv  34644  ballotlem1  34647  ballotlem8  34697  circlemethhgt  34803  r11  35253  r12  35254  onvf1od  35305  usgrcyclgt2v  35329  iccllysconn  35448  rellysconn  35449  satf00  35572  fmla0  35580  msrid  35743  dfrdg2  35991  dfrdg4  36149  imagesset  36151  elhf  36372  filnetlem3  36578  limsucncmpi  36643  ttciunun  36709  bj-babygodel  36884  bj-idres  37490  taupilem3  37649  icoreresf  37682  icoreelrnab  37684  relowlssretop  37693  poimirlem3  37958  poimirlem9  37964  poimirlem15  37970  poimirlem16  37971  poimirlem17  37972  poimirlem19  37974  poimirlem27  37982  poimirlem28  37983  poimirlem31  37986  poimirlem32  37987  mblfinlem1  37992  ovoliunnfl  37997  voliunnfl  37999  mbfresfi  38001  dvtan  38005  itg2addnc  38009  ftc1anclem3  38030  areacirc  38048  fdc  38080  ismrer1  38173  reheibor  38174  rngomndo  38270  gidsn  38287  ac6s6f  38508  cnvref4  38685  dfcnvrefrels2  38943  dfcnvrefrels3  38944  dedths  39422  tendo0co2  41248  erng1r  41455  dvalveclem  41485  dva0g  41487  dvh0g  41571  sn-it0e0  42862  sn-0tie0  42910  2rexfrabdioph  43242  3rexfrabdioph  43243  4rexfrabdioph  43244  6rexfrabdioph  43245  7rexfrabdioph  43246  rencldnfi  43267  jm2.27dlem2  43456  wepwso  43489  dfac11  43508  pwssplit4  43535  frlmpwfi  43544  isnumbasgrplem3  43551  mpaaeu  43596  proot1mul  43640  proot1hash  43641  epirron  43700  oneptr  43701  ordeldif1o  43706  oaomoencom  43763  oenassex  43764  cnvcnvintabd  44045  cnvrcl0  44070  dfrtrcl5  44074  cotrcltrcl  44170  frege92  44400  seff  44754  prmunb2  44756  binomcxplemdvbinom  44798  binomcxplemcvg  44799  binomcxplemnotnn0  44801  permac8prim  45459  sumsnd  45475  islptre  46067  stoweidlem34  46480  stoweidlem37  46483  stirlinglem11  46530  stirlinglem12  46531  stirlinglem13  46532  fouriersw  46677  natlocalincr  47322  nthrucw  47332  fundcmpsurbijinjpreimafv  47879  fundcmpsurinjimaid  47883  fmtnoinf  48011  gbowge7  48251  nnsum3primes4  48276  usgrexmpl12ngrlic  48527  gpgprismgr4cycllem2  48584  gpg5ngric  48616  2zrng0  48732  lmodn0  48983  zlmodzxzldeplem3  48990  lvecpsslmod  48995  0dig2pr01  49098  nelsubc3lem  49557  aacllem  50288  amgmwlem  50289