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  1641  dtruALT2  5326  intasym  6099  relcoi2  6260  funres11  6594  cnvresid  6596  find  7872  fparlem1  8086  fparlem2  8087  dftpos4  8220  tposf12  8226  tfr2b  8362  tz7.44lem1  8371  ord3  8448  xp01disjl  8456  on2recsfn  8632  on2recsov  8633  on2ind  8634  on3ind  8635  xpcomco  9035  sbthlem2  9056  fidomdm  9274  brwdom2  9518  epnsym  9561  inf3lem6  9585  cnfcom  9652  ttrclco  9670  ttrclselem2  9678  tz9.1c  9682  frr1  9714  r1tr  9731  r1ord3g  9734  rankwflemb  9748  r1elwf  9751  r1elss  9761  rankval3b  9781  onssr1  9786  inlresf  9869  inrresf  9871  djuin  9873  infxpenlem  9966  alephnbtwn  10024  alephordilem1  10026  alephfp  10061  dfac13  10096  pwsdompw  10156  infdjuabs  10158  ackbij1  10190  ackbij2  10195  r1om  10196  cflim2  10217  fin23lem27  10282  fin23lem29  10295  fin23lem30  10296  fin1a2lem6  10359  fin1a2lem7  10360  fin1a2lem13  10366  itunitc1  10374  itunitc  10375  ituniiun  10376  hsmexlem5  10384  axcc2lem  10390  axcc3  10392  zorn2lem6  10455  zorn2lem7  10456  ttukeylem6  10468  dmct  10478  iunfo  10493  cardval  10500  cardid  10501  alephom  10540  canthp1lem2  10608  gchaleph2  10627  r1limwun  10691  inaprc  10791  nqerf  10885  recmulnq  10919  dmrecnq  10923  halfnq  10931  genpdm  10957  reclem3pr  11004  axresscn  11103  axpre-sup  11124  1re  11178  0re  11180  00id  11355  addrid  11360  0cnALT  11415  renegcli  11489  zexALT  12585  uzn0  12853  xrinfmss  13310  axdc4uzlem  13993  facnn  14285  fac0  14286  hashgval  14343  hashinf  14345  hashresfn  14350  hashrabrsn  14382  hashrabsn01  14383  hashrabsn1  14384  hashp1i  14413  hash1snb  14429  hashxplem  14443  fi1uzind  14517  cshw1  14832  cats1fv  14869  s7f1o  14976  trclubgi  15007  cnrecnv  15175  rexanuz  15356  climdm  15564  lo1eq  15578  rlimeq  15579  sumsnf  15753  tanval  16143  rpnnen2lem11  16239  rpnnen  16242  sadadd2lem  16476  sadadd3  16478  sadaddlem  16483  sadasslem  16487  sadeq  16489  lcmgcdlem  16623  unbenlem  16927  prmreclem6  16940  vdwlem8  17007  vdwnnlem1  17014  0ram  17039  structcnvcnv  17172  prdsvallem  17466  prdsval  17467  prdsbas  17469  prdsplusg  17470  prdsmulr  17471  prdsvsca  17472  prdshom  17479  xpsfrn  17581  xpsff1o2  17582  catcoppccl  18133  catcfuccl  18134  catcxpccl  18222  tsrss  18604  gsumpropd2lem  18696  smndex2dnrinv  18935  mvdco  19468  efgmnvl  19737  efgval  19740  efgi0  19743  efgi1  19744  efgredeu  19775  0frgp  19802  abln0  19890  lt6abl  19918  gsumval3  19930  gsum2dlem2  19994  dprdres  20053  dmdprdsplit2lem  20070  ringn0  20340  isdrng2  20772  drngmclOLD  20780  drngid2  20781  cnfldplusf  21431  cnfldsub  21432  cnsubmlem  21447  cnsubglem  21448  cnmsubglem  21462  gzrngunitlem  21464  rge0srg  21470  zring0  21490  pzriprnglem10  21522  zzngim  21584  zrhpsgnmhm  21616  re0g  21644  pjfval  21738  pjpm  21740  psrplusg  21969  coe1sfi  22255  ply1plusgfvi  22283  marep01ma  22700  smadiadetlem1a  22703  smadiadetlem3lem2  22707  smadiadetlem3  22708  smadiadetlem4  22709  smadiadet  22710  indistpsALT  23053  tgrest  23199  leordtval2  23252  lmbr2  23299  cnprest  23329  lmff  23341  kgenidm  23587  tx1cn  23649  tx2cn  23650  ustbas  24267  psmetge0  24352  xmetge0  24384  qdensere  24809  cnblcld  24814  cnfldms  24815  cnfldtopn  24821  xrsdsre  24851  xrge0tsms  24875  iccpnfcnv  24986  xrhmeo  24988  cnheiborlem  24996  cnlmod  25182  recvs  25188  lmmbr2  25301  lmcau  25355  metsscmetcld  25357  cncms  25397  cnfldcusp  25399  ovolctb  25532  ovoliunnul  25549  ismbl  25568  volf  25571  voliunlem1  25592  ioorf  25615  ioorinv  25618  ioorcl  25619  dyaddisj  25638  dyadmax  25640  dyadmbl  25642  mbfid  25677  ismbfd  25681  mbfimaopnlem  25697  limcresi  25927  dvreslem  25951  dvres2lem  25952  dvcjbr  25991  dvferm1  26027  dvferm2  26029  dvlip2  26037  dv11cn  26043  deg1ldg  26132  deg1leb  26135  plycpn  26330  vieta1lem2  26352  elqaa  26363  aalioulem2  26374  aaliou3lem3  26385  aaliou3lem4  26387  pserulm  26462  psercnlem2  26464  psercnlem1  26465  psercn  26466  abelth  26481  reeff1o  26487  pilem1  26491  efhalfpi  26513  coseq0negpitopi  26545  pige3ALT  26562  tanregt0  26581  efif1olem3  26586  efif1olem4  26587  efifo  26589  eff1olem  26590  efsubm  26593  logrn  26600  ellogrn  26601  relogf1o  26608  argregt0  26652  argrege0  26653  dvrelog  26679  dvloglem  26690  logf1o2  26692  dvlog  26693  efopnlem1  26698  efopnlem2  26699  logtayl  26702  cxpcn3lem  26789  cxpcn3  26790  resqrtcn  26791  asinneg  26928  asinrebnd  26943  atan0  26950  atanbnd  26968  areambl  27000  sqrtlim  27014  amgmlem  27031  lgamucov  27079  basellem1  27122  basellem4  27125  sqff1o  27223  dchrplusg  27288  bposlem6  27330  bposlem8  27332  dchrvmasumlem2  27539  pntibndlem1  27630  pntlemo  27648  qrng0  27662  ostth  27680  noextendseq  27708  bday0  27881  oldlim  27957  ons2ind  28345  zsex  28450  lmif  28931  islmib  28933  structiedg0val  29169  snstriedgval  29185  umgredgnlp  29294  usgrexmplef  29406  usgrexmpledg  29409  vtxdlfgrval  29632  upgr2pthnlp  29878  konigsberglem5  30404  ex-mod  30597  nowisdomv  30622  pliguhgr  30635  grporn  30670  ip0i  30974  ubthlem1  31019  ubthlem2  31020  axhcompl-zf  31147  normlem7  31265  bcseqi  31269  bcsiALT  31328  hlimf  31386  hlimuni  31387  hhssabloilem  31410  hhshsslem1  31416  hhsssh  31418  hhsscms  31427  occllem  31452  occl  31453  h1deoi  31698  h1dei  31699  h1de2ctlem  31704  h1de2ci  31705  spansni  31706  spanunsni  31728  pjpythi  31871  nmfn0  32136  nmopadjlem  32238  adjcoi  32249  nmopcoadji  32250  pjoccoi  32327  shatomistici  32510  iuninc  32709  imadifxp  32750  xppreima  32797  1stpreima  32859  2ndpreima  32860  fsuppcurry1  32876  fsuppcurry2  32877  hashgt1  32960  s3clhash  33087  gsummpt2d  33190  xrge0tsmsd  33214  tocyc01  33259  cyc3evpm  33291  cycpmconjslem2  33296  cyc3conja  33298  reofld  33490  rearchi  33493  nn0archi  33494  xrge0slmod  33495  elrspunidl  33575  dimval  33859  dimvalfi  33860  ply1degltdimlem  33880  algextdeglem8  33982  qtophaus  34094  iistmd  34160  xpinpreima  34164  xpinpreima2  34165  tpr2rico  34170  mndpluscn  34184  xrge0pluscn  34198  cnzh  34226  rezh  34227  qqhucn  34250  rrhcn  34255  cnrrext  34268  zrhre  34277  qqhre  34278  ismntop  34284  sigaex  34368  brsiga  34441  cntnevol  34486  voliune  34487  ddemeas  34494  1stmbfm  34518  2ndmbfm  34519  br2base  34527  dya2icoseg2  34536  dya2iocucvr  34542  carsgclctunlem2  34577  carsgclctunlem3  34578  sitgaddlemb  34606  eulerpartlemt  34629  eulerpartgbij  34630  eulerpartlemmf  34633  eulerpartlemgvv  34634  eulerpartlemgf  34637  eulerpart  34640  sseqmw  34649  sseqf  34650  sseqp1  34653  fiblem  34656  fibp1  34659  dstrvprob  34730  coinflipspace  34739  coinfliprv  34741  coinflippv  34742  ballotlem1  34745  ballotlem8  34795  circlemethhgt  34901  r11  35354  r12  35355  onvf1od  35414  usgrcyclgt2v  35445  iccllysconn  35564  rellysconn  35565  satf00  35688  fmla0  35696  msrid  35859  dfrdg2  36107  dfrdg4  36265  imagesset  36267  elhf  36488  filnetlem3  36704  limsucncmpi  36769  ttciunun  36835  bj-babygodel  37010  bj-idres  37616  taupilem3  37775  icoreresf  37810  icoreelrnab  37812  relowlssretop  37821  poimirlem3  38086  poimirlem9  38092  poimirlem15  38098  poimirlem16  38099  poimirlem17  38100  poimirlem19  38102  poimirlem27  38110  poimirlem28  38111  poimirlem31  38114  poimirlem32  38115  mblfinlem1  38120  ovoliunnfl  38125  voliunnfl  38127  mbfresfi  38129  dvtan  38133  itg2addnc  38137  ftc1anclem3  38158  areacirc  38176  fdc  38208  ismrer1  38301  reheibor  38302  rngomndo  38398  gidsn  38415  ac6s6f  38636  cnvref4  38813  dfcnvrefrels2  39071  dfcnvrefrels3  39072  dedths  39550  tendo0co2  41376  erng1r  41583  dvalveclem  41613  dva0g  41615  dvh0g  41699  sn-it0e0  42989  sn-0tie0  43037  2rexfrabdioph  43337  3rexfrabdioph  43338  4rexfrabdioph  43339  6rexfrabdioph  43340  7rexfrabdioph  43341  rencldnfi  43362  jm2.27dlem2  43551  wepwso  43584  dfac11  43603  pwssplit4  43630  frlmpwfi  43639  isnumbasgrplem3  43646  mpaaeu  43691  proot1mul  43735  proot1hash  43736  epirron  43795  oneptr  43796  ordeldif1o  43801  oaomoencom  43858  oenassex  43859  cnvcnvintabd  44140  cnvrcl0  44165  dfrtrcl5  44169  cotrcltrcl  44265  frege92  44495  seff  44849  prmunb2  44851  binomcxplemdvbinom  44893  binomcxplemcvg  44894  binomcxplemnotnn0  44896  permac8prim  45554  sumsnd  45570  islptre  46159  stoweidlem34  46572  stoweidlem37  46575  stirlinglem11  46622  stirlinglem12  46623  stirlinglem13  46624  fouriersw  46769  natlocalincr  47416  nthrucw  47426  fundcmpsurbijinjpreimafv  47977  fundcmpsurinjimaid  47981  fmtnoinf  48109  gbowge7  48349  nnsum3primes4  48374  usgrexmpl12ngrlic  48625  gpgprismgr4cycllem2  48682  gpg5ngric  48714  2zrng0  48830  lmodn0  49081  zlmodzxzldeplem3  49088  lvecpsslmod  49093  0dig2pr01  49196  nelsubc3lem  49655  aacllem  50386  amgmwlem  50387