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  3494  dtruALT2  5317  intasym  6080  relcoi2  6243  funres11  6577  cnvresid  6579  find  7847  fparlem1  8064  fparlem2  8065  dftpos4  8197  tposf12  8203  tfr2b  8337  tz7.44lem1  8346  ord3  8422  xp01disjl  8429  on2recsfn  8605  on2recsov  8606  on2ind  8607  on3ind  8608  xpcomco  9007  sbthlem2  9028  fidomdm  9246  brwdom2  9490  epnsym  9530  inf3lem6  9554  cnfcom  9621  ttrclco  9639  ttrclselem2  9647  tz9.1c  9651  frr1  9683  r1tr  9700  r1ord3g  9703  rankwflemb  9717  r1elwf  9720  r1elss  9730  rankval3b  9750  onssr1  9755  inlresf  9838  inrresf  9840  djuin  9842  infxpenlem  9935  alephnbtwn  9993  alephordilem1  9995  alephfp  10030  dfac13  10065  pwsdompw  10125  infdjuabs  10127  ackbij1  10159  ackbij2  10164  r1om  10165  cflim2  10185  fin23lem27  10250  fin23lem29  10263  fin23lem30  10264  fin1a2lem6  10327  fin1a2lem7  10328  fin1a2lem13  10334  itunitc1  10342  itunitc  10343  ituniiun  10344  hsmexlem5  10352  axcc2lem  10358  axcc3  10360  zorn2lem6  10423  zorn2lem7  10424  ttukeylem6  10436  dmct  10446  iunfo  10461  cardval  10468  cardid  10469  alephom  10508  canthp1lem2  10576  gchaleph2  10595  r1limwun  10659  inaprc  10759  nqerf  10853  recmulnq  10887  dmrecnq  10891  halfnq  10899  genpdm  10925  reclem3pr  10972  axresscn  11071  axpre-sup  11092  1re  11144  0re  11146  00id  11320  addrid  11325  0cnALT  11380  renegcli  11454  zexALT  12520  uzn0  12780  xrinfmss  13237  axdc4uzlem  13918  facnn  14210  fac0  14211  hashgval  14268  hashinf  14270  hashresfn  14275  hashrabrsn  14307  hashrabsn01  14308  hashrabsn1  14309  hashp1i  14338  hash1snb  14354  hashxplem  14368  fi1uzind  14442  cshw1  14757  cats1fv  14794  s7f1o  14901  trclubgi  14932  cnrecnv  15100  rexanuz  15281  climdm  15489  lo1eq  15503  rlimeq  15504  sumsnf  15678  tanval  16065  rpnnen2lem11  16161  rpnnen  16164  sadadd2lem  16398  sadadd3  16400  sadaddlem  16405  sadasslem  16409  sadeq  16411  lcmgcdlem  16545  unbenlem  16848  prmreclem6  16861  vdwlem8  16928  vdwnnlem1  16935  0ram  16960  structcnvcnv  17092  prdsvallem  17386  prdsval  17387  prdsbas  17389  prdsplusg  17390  prdsmulr  17391  prdsvsca  17392  prdshom  17399  xpsfrn  17501  xpsff1o2  17502  catcoppccl  18053  catcfuccl  18054  catcxpccl  18142  tsrss  18524  gsumpropd2lem  18616  smndex2dnrinv  18852  mvdco  19386  efgmnvl  19655  efgval  19658  efgi0  19661  efgi1  19662  efgredeu  19693  0frgp  19720  abln0  19808  lt6abl  19836  gsumval3  19848  gsum2dlem2  19912  dprdres  19971  dmdprdsplit2lem  19988  ringn0  20258  isdrng2  20688  drngmclOLD  20696  drngid2  20697  cnfldplusf  21363  cnfldsub  21364  cnsubmlem  21381  cnsubglem  21382  cnmsubglem  21397  gzrngunitlem  21399  rge0srg  21405  zring0  21425  pzriprnglem10  21457  zzngim  21519  zrhpsgnmhm  21551  re0g  21579  pjfval  21673  pjpm  21675  psrplusg  21904  coe1sfi  22166  ply1plusgfvi  22194  marep01ma  22616  smadiadetlem1a  22619  smadiadetlem3lem2  22623  smadiadetlem3  22624  smadiadetlem4  22625  smadiadet  22626  indistpsALT  22969  tgrest  23115  leordtval2  23168  lmbr2  23215  cnprest  23245  lmff  23257  kgenidm  23503  tx1cn  23565  tx2cn  23566  ustbas  24183  psmetge0  24268  xmetge0  24300  qdensere  24725  cnblcld  24730  cnfldms  24731  cnfldtopn  24737  xrsdsre  24767  xrge0tsms  24791  iccpnfcnv  24910  xrhmeo  24912  cnheiborlem  24921  cnlmod  25108  recvs  25114  lmmbr2  25227  lmcau  25281  metsscmetcld  25283  cncms  25323  cnfldcusp  25325  ovolctb  25459  ovoliunnul  25476  ismbl  25495  volf  25498  voliunlem1  25519  ioorf  25542  ioorinv  25545  ioorcl  25546  dyaddisj  25565  dyadmax  25567  dyadmbl  25569  mbfid  25604  ismbfd  25608  mbfimaopnlem  25624  limcresi  25854  dvreslem  25878  dvres2lem  25879  dvcjbr  25921  dvferm1  25957  dvferm2  25959  dvlip2  25968  dv11cn  25974  deg1ldg  26065  deg1leb  26068  plycpn  26265  vieta1lem2  26287  elqaa  26298  aalioulem2  26309  aaliou3lem3  26320  aaliou3lem4  26322  pserulm  26399  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  26725  cxpcn3  26726  resqrtcn  26727  asinneg  26864  asinrebnd  26879  atan0  26886  atanbnd  26904  areambl  26936  sqrtlim  26951  amgmlem  26968  lgamucov  27016  basellem1  27059  basellem4  27062  sqff1o  27160  dchrplusg  27226  bposlem6  27268  bposlem8  27270  dchrvmasumlem2  27477  pntibndlem1  27568  pntlemo  27586  qrng0  27600  ostth  27618  noextendseq  27647  bday0  27819  oldlim  27895  ons2ind  28283  zsex  28388  lmif  28869  islmib  28871  structiedg0val  29107  snstriedgval  29123  umgredgnlp  29232  usgrexmplef  29344  usgrexmpledg  29347  vtxdlfgrval  29571  upgr2pthnlp  29817  konigsberglem5  30343  ex-mod  30536  pliguhgr  30573  grporn  30608  ip0i  30912  ubthlem1  30957  ubthlem2  30958  axhcompl-zf  31085  normlem7  31203  bcseqi  31207  bcsiALT  31266  hlimf  31324  hlimuni  31325  hhssabloilem  31348  hhshsslem1  31354  hhsssh  31356  hhsscms  31365  occllem  31390  occl  31391  h1deoi  31636  h1dei  31637  h1de2ctlem  31642  h1de2ci  31643  spansni  31644  spanunsni  31666  pjpythi  31809  nmfn0  32074  nmopadjlem  32176  adjcoi  32187  nmopcoadji  32188  pjoccoi  32265  shatomistici  32448  iuninc  32646  imadifxp  32687  xppreima  32734  1stpreima  32796  2ndpreima  32797  fsuppcurry1  32813  fsuppcurry2  32814  hashgt1  32898  s3clhash  33040  gsummpt2d  33142  xrge0tsmsd  33166  tocyc01  33211  cyc3evpm  33243  cycpmconjslem2  33248  cyc3conja  33250  reofld  33435  rearchi  33438  nn0archi  33439  xrge0slmod  33440  elrspunidl  33520  dimval  33777  dimvalfi  33778  ply1degltdimlem  33799  algextdeglem8  33901  qtophaus  34013  iistmd  34079  xpinpreima  34083  xpinpreima2  34084  tpr2rico  34089  mndpluscn  34103  xrge0pluscn  34117  cnzh  34145  rezh  34146  qqhucn  34169  rrhcn  34174  cnrrext  34187  zrhre  34196  qqhre  34197  ismntop  34203  sigaex  34287  brsiga  34360  cntnevol  34405  voliune  34406  ddemeas  34413  1stmbfm  34437  2ndmbfm  34438  br2base  34446  dya2icoseg2  34455  dya2iocucvr  34461  carsgclctunlem2  34496  carsgclctunlem3  34497  sitgaddlemb  34525  eulerpartlemt  34548  eulerpartgbij  34549  eulerpartlemmf  34552  eulerpartlemgvv  34553  eulerpartlemgf  34556  eulerpart  34559  sseqmw  34568  sseqf  34569  sseqp1  34572  fiblem  34575  fibp1  34578  dstrvprob  34649  coinflipspace  34658  coinfliprv  34660  coinflippv  34661  ballotlem1  34664  ballotlem8  34714  circlemethhgt  34820  r11  35269  r12  35270  onvf1od  35320  usgrcyclgt2v  35344  iccllysconn  35463  rellysconn  35464  satf00  35587  fmla0  35595  msrid  35758  dfrdg2  36006  dfrdg4  36164  imagesset  36166  elhf  36387  filnetlem3  36593  limsucncmpi  36658  bj-babygodel  36824  bj-idres  37409  taupilem3  37568  icoreresf  37601  icoreelrnab  37603  relowlssretop  37612  poimirlem3  37868  poimirlem9  37874  poimirlem15  37880  poimirlem16  37881  poimirlem17  37882  poimirlem19  37884  poimirlem27  37892  poimirlem28  37893  poimirlem31  37896  poimirlem32  37897  mblfinlem1  37902  ovoliunnfl  37907  voliunnfl  37909  mbfresfi  37911  dvtan  37915  itg2addnc  37919  ftc1anclem3  37940  areacirc  37958  fdc  37990  ismrer1  38083  reheibor  38084  rngomndo  38180  gidsn  38197  ac6s6f  38418  cnvref4  38595  dfcnvrefrels2  38853  dfcnvrefrels3  38854  dedths  39332  tendo0co2  41158  erng1r  41365  dvalveclem  41395  dva0g  41397  dvh0g  41481  sn-it0e0  42780  sn-0tie0  42815  2rexfrabdioph  43147  3rexfrabdioph  43148  4rexfrabdioph  43149  6rexfrabdioph  43150  7rexfrabdioph  43151  rencldnfi  43172  jm2.27dlem2  43361  wepwso  43394  dfac11  43413  pwssplit4  43440  frlmpwfi  43449  isnumbasgrplem3  43456  mpaaeu  43501  proot1mul  43545  proot1hash  43546  epirron  43605  oneptr  43606  ordeldif1o  43611  oaomoencom  43668  oenassex  43669  cnvcnvintabd  43950  cnvrcl0  43975  dfrtrcl5  43979  cotrcltrcl  44075  frege92  44305  seff  44659  prmunb2  44661  binomcxplemdvbinom  44703  binomcxplemcvg  44704  binomcxplemnotnn0  44706  permac8prim  45364  sumsnd  45380  islptre  45973  stoweidlem34  46386  stoweidlem37  46389  stirlinglem11  46436  stirlinglem12  46437  stirlinglem13  46438  fouriersw  46583  natlocalincr  47228  nthrucw  47238  fundcmpsurbijinjpreimafv  47761  fundcmpsurinjimaid  47765  fmtnoinf  47890  gbowge7  48117  nnsum3primes4  48142  usgrexmpl12ngrlic  48393  gpgprismgr4cycllem2  48450  gpg5ngric  48482  2zrng0  48598  lmodn0  48849  zlmodzxzldeplem3  48856  lvecpsslmod  48861  0dig2pr01  48964  nelsubc3lem  49423  aacllem  50154  amgmwlem  50155