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  1645  dtruALT2  5332  intasym  6106  relcoi2  6268  funres11  6602  cnvresid  6604  find  7880  fparlem1  8095  fparlem2  8096  dftpos4  8229  tposf12  8235  tfr2b  8371  tz7.44lem1  8380  ord3  8457  xp01disjl  8465  on2recsfn  8641  on2recsov  8642  on2ind  8643  on3ind  8644  xpcomco  9043  sbthlem2  9064  fidomdm  9279  brwdom2  9523  epnsym  9566  inf3lem6  9590  cnfcom  9657  ttrclco  9675  ttrclselem2  9683  tz9.1c  9687  frr1  9719  r1tr  9736  r1ord3g  9739  rankwflemb  9753  r1elwf  9756  r1elss  9766  rankval3b  9786  onssr1  9791  inlresf  9888  inrresf  9890  djuin  9892  infxpenlem  9985  alephnbtwn  10043  alephordilem1  10045  alephfp  10080  dfac13  10114  pwsdompw  10174  infdjuabs  10176  ackbij1  10208  ackbij2  10213  r1om  10214  cflim2  10235  fin23lem27  10300  fin23lem29  10313  fin23lem30  10314  fin1a2lem6  10377  fin1a2lem7  10378  fin1a2lem13  10384  itunitc1  10392  itunitc  10393  ituniiun  10394  hsmexlem5  10402  axcc2lem  10408  axcc3  10410  zorn2lem6  10473  zorn2lem7  10474  ttukeylem6  10486  dmct  10496  iunfo  10511  cardval  10518  cardid  10519  alephom  10558  canthp1lem2  10626  gchaleph2  10645  r1limwun  10709  inaprc  10809  nqerf  10903  recmulnq  10937  dmrecnq  10941  halfnq  10949  genpdm  10975  reclem3pr  11022  axresscn  11121  axpre-sup  11142  1re  11196  0re  11198  00id  11373  addrid  11378  0cnALT  11433  renegcli  11507  zexALT  12602  uzn0  12870  xrinfmss  13327  axdc4uzlem  14010  facnn  14302  fac0  14303  hashgval  14360  hashinf  14362  hashresfn  14367  hashrabrsn  14399  hashrabsn01  14400  hashrabsn1  14401  hashp1i  14430  hash1snb  14446  hashxplem  14460  fi1uzind  14534  cshw1  14849  cats1fv  14886  s7f1o  14993  trclubgi  15024  cnrecnv  15206  rexanuz  15387  climdm  15595  lo1eq  15609  rlimeq  15610  sumsnf  15784  tanval  16174  rpnnen2lem11  16270  rpnnen  16273  sadadd2lem  16507  sadadd3  16509  sadaddlem  16514  sadasslem  16518  sadeq  16520  lcmgcdlem  16654  unbenlem  16958  prmreclem6  16971  vdwlem8  17038  vdwnnlem1  17045  0ram  17070  structcnvcnv  17203  prdsvallem  17497  prdsval  17498  prdsbas  17500  prdsplusg  17501  prdsmulr  17502  prdsvsca  17503  prdshom  17510  xpsfrn  17612  xpsff1o2  17613  catcoppccl  18164  catcfuccl  18165  catcxpccl  18253  tsrss  18635  gsumpropd2lem  18727  smndex2dnrinv  18967  mvdco  19506  efgmnvl  19775  efgval  19778  efgi0  19781  efgi1  19782  efgredeu  19813  0frgp  19840  abln0  19928  lt6abl  19956  gsumval3  19968  gsum2dlem2  20032  dprdres  20091  dmdprdsplit2lem  20108  ringn0  20385  isdrng2  20818  drngid2  20826  cnfldplusf  21509  cnfldsub  21510  cnsubmlem  21525  cnsubglem  21526  cnmsubglem  21540  gzrngunitlem  21542  rge0srg  21548  zring0  21568  pzriprnglem10  21600  zzngim  21662  zrhpsgnmhm  21694  re0g  21722  pjfval  21816  pjpm  21818  psrplusg  22047  coe1sfi  22333  ply1plusgfvi  22361  marep01ma  22778  smadiadetlem1a  22781  smadiadetlem3lem2  22785  smadiadetlem3  22786  smadiadetlem4  22787  smadiadet  22788  indistpsALT  23131  tgrest  23277  leordtval2  23330  lmbr2  23377  cnprest  23407  lmff  23419  kgenidm  23665  tx1cn  23727  tx2cn  23728  ustbas  24345  psmetge0  24430  xmetge0  24462  qdensere  24887  cnblcld  24892  cnfldms  24893  cnfldtopn  24899  xrsdsre  24929  xrge0tsms  24953  iccpnfcnv  25064  xrhmeo  25066  cnheiborlem  25074  cnlmod  25260  recvs  25266  lmmbr2  25379  lmcau  25433  metsscmetcld  25435  cncms  25475  cnfldcusp  25477  ovolctb  25610  ovoliunnul  25627  ismbl  25646  volf  25649  voliunlem1  25670  ioorf  25693  ioorinv  25696  ioorcl  25697  dyaddisj  25716  dyadmax  25718  dyadmbl  25720  mbfid  25755  ismbfd  25759  mbfimaopnlem  25775  limcresi  26005  dvreslem  26029  dvres2lem  26030  dvcjbr  26069  dvferm1  26105  dvferm2  26107  dvlip2  26115  dv11cn  26121  deg1ldg  26210  deg1leb  26213  plycpn  26411  vieta1lem2  26433  elqaa  26444  aalioulem2  26455  aaliou3lem3  26466  aaliou3lem4  26468  pserulm  26543  psercnlem2  26545  psercnlem1  26546  psercn  26547  abelth  26562  reeff1o  26568  pilem1  26572  efhalfpi  26594  coseq0negpitopi  26626  pige3ALT  26643  tanregt0  26662  efif1olem3  26667  efif1olem4  26668  efifo  26670  eff1olem  26671  efsubm  26674  logrn  26681  ellogrn  26682  relogf1o  26689  argregt0  26733  argrege0  26734  dvrelog  26760  dvloglem  26771  logf1o2  26773  dvlog  26774  efopnlem1  26779  efopnlem2  26780  logtayl  26783  cxpcn3lem  26870  cxpcn3  26871  resqrtcn  26872  asinneg  27009  asinrebnd  27024  atan0  27031  atanbnd  27049  areambl  27081  sqrtlim  27095  amgmlem  27112  lgamucov  27160  basellem1  27203  basellem4  27206  sqff1o  27304  dchrplusg  27369  bposlem6  27411  bposlem8  27413  dchrvmasumlem2  27620  pntibndlem1  27711  pntlemo  27729  qrng0  27743  ostth  27761  noextendseq  27789  bday0  27962  oldlim  28038  ons2ind  28426  zsex  28531  lmif  29037  islmib  29039  structiedg0val  29281  snstriedgval  29297  umgredgnlp  29406  usgrexmplef  29518  usgrexmpledg  29521  vtxdlfgrval  29744  upgr2pthnlp  29990  konigsberglem5  30516  ex-mod  30709  nowisdomv  30734  pliguhgr  30747  grporn  30782  ip0i  31086  ubthlem1  31131  ubthlem2  31132  axhcompl-zf  31259  normlem7  31377  bcseqi  31381  bcsiALT  31440  hlimf  31498  hlimuni  31499  hhssabloilem  31522  hhshsslem1  31528  hhsssh  31530  hhsscms  31539  occllem  31564  occl  31565  h1deoi  31810  h1dei  31811  h1de2ctlem  31816  h1de2ci  31817  spansni  31818  spanunsni  31840  pjpythi  31983  nmfn0  32248  nmopadjlem  32350  adjcoi  32361  nmopcoadji  32362  pjoccoi  32439  shatomistici  32622  iuninc  32815  imadifxp  32856  xppreima  32902  1stpreima  32964  2ndpreima  32965  fsuppcurry1  32981  fsuppcurry2  32982  hashgt1  33065  s3clhash  33181  gsummpt2d  33282  xrge0tsmsd  33306  tocyc01  33351  cyc3evpm  33383  cycpmconjslem2  33388  cyc3conja  33390  reofld  33578  rearchi  33581  nn0archi  33582  xrge0slmod  33583  elrspunidl  33652  dimval  33908  dimvalfi  33909  ply1degltdimlem  33929  algextdeglem8  34031  qtophaus  34143  iistmd  34209  xpinpreima  34213  xpinpreima2  34214  tpr2rico  34219  mndpluscn  34233  xrge0pluscn  34247  cnzh  34275  rezh  34276  qqhucn  34299  rrhcn  34304  cnrrext  34317  zrhre  34326  qqhre  34327  ismntop  34333  sigaex  34417  brsiga  34490  cntnevol  34535  voliune  34536  ddemeas  34543  1stmbfm  34567  2ndmbfm  34568  br2base  34576  dya2icoseg2  34585  dya2iocucvr  34591  carsgclctunlem2  34626  carsgclctunlem3  34627  sitgaddlemb  34655  eulerpartlemt  34678  eulerpartgbij  34679  eulerpartlemmf  34682  eulerpartlemgvv  34683  eulerpartlemgf  34686  eulerpart  34689  sseqmw  34698  sseqf  34699  sseqp1  34702  fiblem  34705  fibp1  34708  dstrvprob  34779  coinflipspace  34788  coinfliprv  34790  coinflippv  34791  ballotlem1  34794  ballotlem8  34844  circlemethhgt  34947  r11  35402  r12  35403  onvf1od  35462  usgrcyclgt2v  35494  iccllysconn  35613  rellysconn  35614  satf00  35737  fmla0  35745  msrid  35908  dfrdg2  36156  dfrdg4  36314  imagesset  36316  elhf  36537  filnetlem3  36753  limsucncmpi  36818  ttciunun  36884  bj-babygodel  37058  bj-idres  37664  taupilem3  37823  icoreresf  37858  icoreelrnab  37860  relowlssretop  37869  poimirlem3  38134  poimirlem9  38140  poimirlem15  38146  poimirlem16  38147  poimirlem17  38148  poimirlem19  38150  poimirlem27  38158  poimirlem28  38159  poimirlem31  38162  poimirlem32  38163  mblfinlem1  38168  ovoliunnfl  38173  voliunnfl  38175  mbfresfi  38177  dvtan  38181  itg2addnc  38185  ftc1anclem3  38206  areacirc  38224  fdc  38256  ismrer1  38349  reheibor  38350  rngomndo  38446  gidsn  38463  ac6s6f  38684  cnvref4  38861  dfcnvrefrels2  39119  dfcnvrefrels3  39120  dedths  39598  tendo0co2  41424  erng1r  41631  dvalveclem  41661  dva0g  41663  dvh0g  41747  sn-it0e0  43037  sn-0tie0  43085  2rexfrabdioph  43385  3rexfrabdioph  43386  4rexfrabdioph  43387  6rexfrabdioph  43388  7rexfrabdioph  43389  rencldnfi  43410  jm2.27dlem2  43599  wepwso  43632  dfac11  43651  pwssplit4  43678  frlmpwfi  43687  isnumbasgrplem3  43694  mpaaeu  43739  proot1mul  43783  proot1hash  43784  epirron  43843  oneptr  43844  ordeldif1o  43849  oaomoencom  43906  oenassex  43907  cnvcnvintabd  44188  cnvrcl0  44213  dfrtrcl5  44217  cotrcltrcl  44313  frege92  44543  seff  44883  prmunb2  44885  binomcxplemdvbinom  44927  binomcxplemcvg  44928  binomcxplemnotnn0  44930  permac8prim  45588  sumsnd  45604  islptre  46193  stoweidlem34  46606  stoweidlem37  46609  stirlinglem11  46656  stirlinglem12  46657  stirlinglem13  46658  fouriersw  46803  natlocalincr  47450  nthrucw  47460  fundcmpsurbijinjpreimafv  48011  fundcmpsurinjimaid  48015  fmtnoinf  48143  gbowge7  48383  nnsum3primes4  48408  usgrexmpl12ngrlic  48659  gpgprismgr4cycllem2  48716  gpg5ngric  48748  2zrng0  48864  lmodn0  49126  zlmodzxzldeplem3  49133  lvecpsslmod  49138  0dig2pr01  49241  nelsubc3lem  49699  aacllem  50430  amgmwlem  50431