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 ⊢ 𝜒

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5

This theorem is used by:  minimp-syllsimp  1655  dtruALT2  5332  intasym  6107  relcoi2  6273  funres11  6609  cnvresid  6611  find  7896  fparlem1  8112  fparlem2  8113  dftpos4  8246  tposf12  8252  tfr2b  8388  tz7.44lem1  8397  ord3  8476  xp01disjl  8484  on2recsfn  8660  on2recsov  8661  on2ind  8662  on3ind  8663  xpcomco  9070  sbthlem2  9091  fidomdm  9307  brwdom2  9551  epnsym  9594  inf3lem6  9618  cnfcom  9685  ttrclco  9703  ttrclselem2  9711  tz9.1c  9715  frr1  9747  r1tr  9766  r1ord3g  9769  rankwflemb  9783  r1elwf  9786  r1elss  9796  rankval3b  9817  onssr1  9824  elhfOLD  9889  inlresf  9976  inrresf  9978  djuin  9980  infxpenlem  10073  alephnbtwn  10131  alephordilem1  10133  alephfp  10168  dfac13  10202  pwsdompw  10262  infdjuabs  10264  ackbij1  10296  ackbij2  10301  cflim2  10322  fin23lem27  10387  fin23lem29  10400  fin23lem30  10401  fin1a2lem6  10464  fin1a2lem7  10465  fin1a2lem13  10471  itunitc1  10479  itunitc  10480  ituniiun  10481  hsmexlem5  10489  axcc2lem  10495  axcc3  10497  zorn2lem6  10560  zorn2lem7  10561  ttukeylem6  10573  dmct  10583  dmctOLD  10584  iunfo  10604  cardval  10611  cardid  10612  alephom  10651  canthp1lem2  10719  gchaleph2  10738  r1limwun  10802  inaprc  10902  nqerf  10996  recmulnq  11030  dmrecnq  11034  halfnq  11042  genpdm  11068  reclem3pr  11115  axresscn  11214  axpre-sup  11235  1re  11289  0re  11291  00id  11466  addrid  11471  0cnALT  11526  renegcli  11600  zexALT  12694  uzn0  12963  xrinfmss  13421  axdc4uzlem  14106  facnn  14399  fac0  14400  hashgval  14457  hashinf  14459  hashresfn  14464  hashrabrsn  14496  hashrabsn01  14497  hashrabsn1  14498  hashp1i  14527  hash1snb  14544  hashxplem  14558  fi1uzind  14632  cshw1  14953  cats1fv  14990  s7f1o  15099  trclubgi  15130  cnrecnv  15312  rexanuz  15493  climdm  15701  lo1eq  15715  rlimeq  15716  sumsnf  15889  tanval  16276  rpnnen2lem11  16372  rpnnen  16375  sadadd2lem  16609  sadadd3  16611  sadaddlem  16616  sadasslem  16620  sadeq  16622  lcmgcdlem  16761  unbenlem  17066  prmreclem6  17079  vdwlem8  17146  vdwnnlem1  17153  0ram  17178  structcnvcnv  17311  prdsvallem  17605  prdsval  17606  prdsbas  17608  prdsplusg  17609  prdsmulr  17610  prdsvsca  17611  prdshom  17618  xpsfrn  17720  xpsff1o2  17721  catcoppccl  18272  catcfuccl  18273  catcxpccl  18361  tsrss  18743  gsumpropd2lem  18848  smndex2dnrinv  19094  mvdco  19639  efgmnvl  19908  efgval  19911  efgi0  19914  efgi1  19915  efgredeu  19946  0frgp  19973  abln0  20061  lt6abl  20089  gsumval3  20101  gsum2dlem2  20165  dprdres  20224  dmdprdsplit2lem  20241  ringn0  20522  isdrng2  20977  drngid2  20990  cnfldplusf  21685  cnfldsub  21686  cnsubmlem  21701  cnsubglem  21702  cnmsubglem  21716  gzrngunitlem  21718  rge0srg  21724  zring0  21744  pzriprnglem10  21776  zzngim  21838  zrhpsgnmhm  21870  re0g  21898  pjfval  21992  pjpm  21994  psrplusg  22225  coe1sfi  22511  ply1plusgfvi  22539  marep01ma  22955  smadiadetlem1a  22958  smadiadetlem3lem2  22962  smadiadetlem3  22963  smadiadetlem4  22964  smadiadet  22965  indistpsALT  23311  tgrest  23457  leordtval2  23510  lmbr2  23557  cnprest  23587  lmff  23599  kgenidm  23846  tx1cn  23908  tx2cn  23909  ustbas  24526  psmetge0  24611  xmetge0  24643  qdensere  25068  cnblcld  25073  cnfldms  25074  cnfldtopn  25080  xrsdsre  25110  xrge0tsms  25134  iccpnfcnv  25245  xrhmeo  25247  cnheiborlem  25255  cnlmod  25441  recvs  25447  lmmbr2  25560  lmcau  25614  metsscmetcld  25616  cncms  25656  cnfldcusp  25658  ovolctb  25791  ovoliunnul  25808  ismbl  25827  volf  25830  voliunlem1  25851  ioorf  25874  ioorinv  25877  ioorcl  25878  dyaddisj  25897  dyadmax  25899  dyadmbl  25901  mbfid  25936  ismbfd  25940  mbfimaopnlem  25956  limcresi  26185  dvreslem  26209  dvres2lem  26210  dvcjbr  26249  dvferm1  26285  dvferm2  26287  dvlip2  26295  dv11cn  26301  deg1ldg  26390  deg1leb  26393  plycpn  26592  vieta1lem2  26616  elqaa  26627  aalioulem2  26642  aaliou3lem3  26653  aaliou3lem4  26655  pserulm  26731  psercnlem2  26733  psercnlem1  26734  psercn  26735  abelth  26750  reeff1o  26756  pilem1  26760  efhalfpi  26782  coseq0negpitopi  26814  pige3ALT  26830  tanregt0  26849  efif1olem3  26854  efif1olem4  26855  efifo  26857  eff1olem  26858  efsubm  26861  logrn  26868  ellogrn  26869  relogf1o  26876  argregt0  26920  argrege0  26921  dvrelog  26947  dvloglem  26958  logf1o2  26960  dvlog  26961  efopnlem1  26966  efopnlem2  26967  logtayl  26970  cxpcn3lem  27057  cxpcn3  27058  resqrtcn  27059  asinneg  27196  asinrebnd  27211  atan0  27218  atanbnd  27236  areambl  27268  sqrtlim  27282  amgmlem  27299  lgamucov  27347  basellem1  27390  basellem4  27393  sqff1o  27491  dchrplusg  27556  bposlem6  27598  bposlem8  27600  dchrvmasumlem2  27807  pntibndlem1  27898  pntlemo  27916  qrng0  27930  ostth  27948  noextendseq  28006  bday0  28179  oldlim  28255  ons2ind  28643  zsex  28748  lmif  29272  islmib  29274  structiedg0val  29582  snstriedgval  29598  umgredgnlp  29707  usgrexmplef  29822  usgrexmpledg  29825  vtxdlfgrval  30048  upgr2pthnlp  30300  konigsberglem5  30839  ex-mod  31032  nowisdomv  31057  pliguhgr  31070  grporn  31105  ip0i  31409  ubthlem1  31454  ubthlem2  31455  axhcompl-zf  31582  normlem7  31700  bcseqi  31704  bcsiALT  31763  hlimf  31821  hlimuni  31822  hhssabloilem  31845  hhshsslem1  31851  hhsssh  31853  hhsscms  31862  occllem  31887  occl  31888  h1deoi  32133  h1dei  32134  h1de2ctlem  32139  h1de2ci  32140  spansni  32141  spanunsni  32163  pjpythi  32306  nmfn0  32571  nmopadjlem  32673  adjcoi  32684  nmopcoadji  32685  pjoccoi  32762  shatomistici  32945  iuninc  33137  imadifxp  33177  xppreima  33221  1stpreima  33282  2ndpreima  33283  fsuppcurry1  33298  fsuppcurry2  33299  hashgt1  33382  s3clhash  33494  gsummpt2d  33592  xrge0tsmsd  33616  tocyc01  33661  cyc3evpm  33693  cycpmconjslem2  33698  cyc3conja  33700  reofld  33886  rearchi  33889  nn0archi  33890  xrge0slmod  33891  elrspunidl  33960  dimval  34215  dimvalfi  34216  ply1degltdimlem  34236  algextdeglem8  34338  qtophaus  34450  iistmd  34516  xpinpreima  34520  xpinpreima2  34521  tpr2rico  34526  mndpluscn  34540  xrge0pluscn  34554  cnzh  34582  rezh  34583  qqhucn  34606  rrhcn  34611  cnrrext  34624  zrhre  34633  qqhre  34634  ismntop  34640  sigaex  34724  brsiga  34798  cntnevol  34843  voliune  34844  ddemeas  34851  1stmbfm  34875  2ndmbfm  34876  br2base  34884  dya2icoseg2  34893  dya2iocucvr  34899  carsgclctunlem2  34934  carsgclctunlem3  34935  sitgaddlemb  34963  eulerpartlemt  34986  eulerpartgbij  34987  eulerpartlemmf  34990  eulerpartlemgvv  34991  eulerpartlemgf  34994  eulerpart  34997  sseqmw  35006  sseqf  35007  sseqp1  35010  fiblem  35013  fibp1  35016  dstrvprob  35087  coinflipspace  35096  coinfliprv  35098  coinflippv  35099  ballotlem1  35102  ballotlem8  35152  circlemethhgt  35255  r11  35704  r12  35705  onvf1od  35859  usgrcyclgt2v  35879  iccllysconn  35984  rellysconn  35985  satf00  36108  fmla0  36116  msrid  36279  dfrdg2  36527  dfrdg4  36685  imagesset  36687  filnetlem3  37138  limsucncmpi  37203  ttciunun  37269  bj-babygodel  37443  bj-idres  38049  taupilem3  38208  icoreresf  38243  icoreelrnab  38245  relowlssretop  38254  poimirlem3  38509  poimirlem9  38515  poimirlem15  38521  poimirlem16  38522  poimirlem17  38523  poimirlem19  38525  poimirlem27  38533  poimirlem28  38534  poimirlem31  38537  poimirlem32  38538  mblfinlem1  38543  ovoliunnfl  38548  voliunnfl  38550  mbfresfi  38552  dvtan  38556  itg2addnc  38560  ftc1anclem3  38581  areacirc  38599  fdc  38647  ismrer1  38740  reheibor  38741  rngomndo  38837  gidsn  38854  ac6s6f  39073  cnvref4  39250  dfcnvrefrels2  39508  dfcnvrefrels3  39509  dedths  39987  tendo0co2  41813  erng1r  42020  dvalveclem  42050  dva0g  42052  dvh0g  42136  sn-it0e0  43435  sn-0tie0  43483  2rexfrabdioph  43756  3rexfrabdioph  43757  4rexfrabdioph  43758  6rexfrabdioph  43759  7rexfrabdioph  43760  rencldnfi  43781  jm2.27dlem2  43970  wepwso  44003  dfac11  44022  pwssplit4  44049  frlmpwfi  44058  isnumbasgrplem3  44065  mpaaeu  44110  proot1mul  44154  proot1hash  44155  epirron  44214  oneptr  44215  ordeldif1o  44220  oaomoencom  44277  oenassex  44278  cnvcnvintabd  44559  cnvrcl0  44584  dfrtrcl5  44588  cotrcltrcl  44684  frege92  44914  seff  45252  prmunb2  45254  binomcxplemdvbinom  45296  binomcxplemcvg  45297  binomcxplemnotnn0  45299  permac8prim  45956  sumsnd  45986  islptre  46575  stoweidlem34  46988  stoweidlem37  46991  stirlinglem11  47038  stirlinglem12  47039  stirlinglem13  47040  fouriersw  47185  fundcmpsurbijinjpreimafv  48433  fundcmpsurinjimaid  48437  fmtnoinf  48565  gbowge7  48805  nnsum3primes4  48830  usgrexmpl12ngrlic  49081  gpgprismgr4cycllem2  49138  gpg5ngric  49170  2zrng0  49285  lmodn0  49551  zlmodzxzldeplem3  49558  lvecpsslmod  49563  0dig2pr01  49666  nelsubc3lem  50122  aacllem  50883  amgmwlem  50931