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  1620  ceqsexv2dOLD  3546  dtruALT2  5388  dtruOLD  5461  intasym  6147  relcoi2  6308  funres11  6655  cnvresid  6657  omsindsOLD  7925  find  7935  fparlem1  8153  fparlem2  8154  dftpos4  8286  tposf12  8292  wfrlem14OLD  8378  tfr2b  8452  tz7.44lem1  8461  ord3  8539  xp01disjl  8548  on2recsfn  8723  on2recsov  8724  on2ind  8725  on3ind  8726  xpcomco  9128  sbthlem2  9150  fidomdm  9402  brwdom2  9642  epnsym  9678  inf3lem6  9702  omex  9712  cnfcom  9769  ttrclco  9787  ttrclselem2  9795  tz9.1c  9799  frr1  9828  r1tr  9845  r1ord3g  9848  rankwflemb  9862  r1elwf  9865  r1elss  9875  rankval3b  9895  onssr1  9900  inlresf  9983  inrresf  9985  djuin  9987  infxpenlem  10082  alephnbtwn  10140  alephordilem1  10142  alephfp  10177  dfac13  10212  pwsdompw  10272  infdjuabs  10274  ackbij1  10306  ackbij2  10311  r1om  10312  cflim2  10332  fin23lem27  10397  fin23lem29  10410  fin23lem30  10411  fin1a2lem6  10474  fin1a2lem7  10475  fin1a2lem13  10481  itunitc1  10489  itunitc  10490  ituniiun  10491  hsmexlem5  10499  axcc2lem  10505  axcc3  10507  zorn2lem6  10570  zorn2lem7  10571  ttukeylem6  10583  axdc  10590  dmct  10593  iunfo  10608  cardval  10615  cardid  10616  pwcfsdom  10652  alephom  10654  canthp1lem2  10722  gchaleph2  10741  r1limwun  10805  inaprc  10905  nqerf  10999  recmulnq  11033  dmrecnq  11037  halfnq  11045  genpdm  11071  reclem3pr  11118  axresscn  11217  axpre-sup  11238  1re  11290  0re  11292  00id  11465  addrid  11470  0cnALT  11524  renegcli  11597  zexALT  12659  uzn0  12920  xrinfmss  13372  axdc4uzlem  14034  facnn  14324  fac0  14325  hashgval  14382  hashinf  14384  hashresfn  14389  hashrabrsn  14421  hashrabsn01  14422  hashrabsn1  14423  hashp1i  14452  hash1snb  14468  hashxplem  14482  fi1uzind  14556  cshw1  14870  cats1fv  14908  s7f1o  15015  trclubgi  15046  cnrecnv  15214  rexanuz  15394  climdm  15600  lo1eq  15614  rlimeq  15615  sumsnf  15791  tanval  16176  rpnnen2lem11  16272  rpnnen  16275  sadadd2lem  16505  sadadd3  16507  sadaddlem  16512  sadasslem  16516  sadeq  16518  lcmgcdlem  16653  unbenlem  16955  prmreclem6  16968  vdwlem8  17035  vdwnnlem1  17042  0ram  17067  structcnvcnv  17200  prdsvallem  17514  prdsval  17515  prdsbas  17517  prdsplusg  17518  prdsmulr  17519  prdsvsca  17520  prdshom  17527  xpsfrn  17628  xpsff1o2  17629  catcoppccl  18184  catcoppcclOLD  18185  catcfuccl  18186  catcfucclOLD  18187  catcxpccl  18276  catcxpcclOLD  18277  tsrss  18659  gsumpropd2lem  18717  smndex2dnrinv  18950  mvdco  19487  efgmnvl  19756  efgval  19759  efgi0  19762  efgi1  19763  efgredeu  19794  0frgp  19821  abln0  19909  lt6abl  19937  gsumval3  19949  gsum2dlem2  20013  dprdres  20072  dmdprdsplit2lem  20089  ringn0  20334  isdrng2  20765  drngmclOLD  20773  drngid2  20774  cnfldplusf  21432  cnfldsub  21433  cnsubmlem  21455  cnsubglem  21456  cnmsubglem  21471  gzrngunitlem  21473  rge0srg  21479  zring0  21492  pzriprnglem10  21524  zzngim  21594  zrhpsgnmhm  21625  re0g  21653  pjfval  21749  pjpm  21751  psrplusg  21979  coe1sfi  22236  ply1plusgfvi  22264  marep01ma  22687  smadiadetlem1a  22690  smadiadetlem3lem2  22694  smadiadetlem3  22695  smadiadetlem4  22696  smadiadet  22697  indistpsALT  23041  indistpsALTOLD  23042  tgrest  23188  leordtval2  23241  lmbr2  23288  cnprest  23318  lmff  23330  kgenidm  23576  tx1cn  23638  tx2cn  23639  ustbas  24257  psmetge0  24343  xmetge0  24375  qdensere  24811  cnblcld  24816  cnfldms  24817  cnfldtopn  24823  xrsdsre  24851  xrge0tsms  24875  iccpnfcnv  24994  xrhmeo  24996  cnheiborlem  25005  cnlmod  25192  recvs  25198  lmmbr2  25312  lmcau  25366  metsscmetcld  25368  cncms  25408  cnfldcusp  25410  ovolctb  25544  ovoliunnul  25561  ismbl  25580  volf  25583  voliunlem1  25604  ioorf  25627  ioorinv  25630  ioorcl  25631  dyaddisj  25650  dyadmax  25652  dyadmbl  25654  mbfid  25689  ismbfd  25693  mbfimaopnlem  25709  limcresi  25940  dvreslem  25964  dvres2lem  25965  dvcjbr  26007  dvferm1  26043  dvferm2  26045  dvlip2  26054  dv11cn  26060  deg1ldg  26151  deg1leb  26154  plycpn  26349  vieta1lem2  26371  elqaa  26382  aalioulem2  26393  aaliou3lem3  26404  aaliou3lem4  26406  pserulm  26483  psercnlem2  26486  psercnlem1  26487  psercn  26488  abelth  26503  reeff1o  26509  pilem1  26513  efhalfpi  26531  coseq0negpitopi  26563  pige3ALT  26580  tanregt0  26599  efif1olem3  26604  efif1olem4  26605  efifo  26607  eff1olem  26608  efsubm  26611  logrn  26618  ellogrn  26619  relogf1o  26626  argregt0  26670  argrege0  26671  dvrelog  26697  dvloglem  26708  logf1o2  26710  dvlog  26711  efopnlem1  26716  efopnlem2  26717  logtayl  26720  cxpcn3lem  26808  cxpcn3  26809  resqrtcn  26810  asinneg  26947  asinrebnd  26962  atan0  26969  atanbnd  26987  areambl  27019  sqrtlim  27034  amgmlem  27051  lgamucov  27099  basellem1  27142  basellem4  27145  sqff1o  27243  dchrplusg  27309  bposlem6  27351  bposlem8  27353  dchrvmasumlem2  27560  mulog2sum  27599  pntibndlem1  27651  pntlemo  27669  qrng0  27683  ostth  27701  noextendseq  27730  bday0s  27891  oldlim  27943  zsex  28384  lmif  28811  islmib  28813  structiedg0val  29057  snstriedgval  29073  umgredgnlp  29182  usgrexmplef  29294  usgrexmpledg  29297  vtxdlfgrval  29521  upgr2pthnlp  29768  konigsberglem5  30288  ex-mod  30481  pliguhgr  30518  grporn  30553  ip0i  30857  ubthlem1  30902  ubthlem2  30903  axhcompl-zf  31030  normlem7  31148  bcseqi  31152  bcsiALT  31211  hlimf  31269  hlimuni  31270  hhssabloilem  31293  hhshsslem1  31299  hhsssh  31301  hhsscms  31310  occllem  31335  occl  31336  h1deoi  31581  h1dei  31582  h1de2ctlem  31587  h1de2ci  31588  spansni  31589  spanunsni  31611  pjpythi  31754  nmfn0  32019  nmopadjlem  32121  adjcoi  32132  nmopcoadji  32133  pjoccoi  32210  shatomistici  32393  iuninc  32583  imadifxp  32623  xppreima  32664  1stpreima  32718  2ndpreima  32719  fsuppcurry1  32739  fsuppcurry2  32740  hashgt1  32815  s3clhash  32914  gsummpt2d  33032  xrge0tsmsd  33041  tocyc01  33111  cyc3evpm  33143  cycpmconjslem2  33148  cyc3conja  33150  reofld  33337  rearchi  33339  nn0archi  33340  xrge0slmod  33341  elrspunidl  33421  dimval  33613  dimvalfi  33614  ply1degltdimlem  33635  algextdeglem8  33715  qtophaus  33782  iistmd  33848  xpinpreima  33852  xpinpreima2  33853  tpr2rico  33858  mndpluscn  33872  xrge0pluscn  33886  cnzh  33916  rezh  33917  qqhucn  33938  rrhcn  33943  cnrrext  33956  zrhre  33965  qqhre  33966  ismntop  33972  sigaex  34074  brsiga  34147  cntnevol  34192  voliune  34193  ddemeas  34200  1stmbfm  34225  2ndmbfm  34226  br2base  34234  dya2icoseg2  34243  dya2iocucvr  34249  carsgclctunlem2  34284  carsgclctunlem3  34285  sitgaddlemb  34313  eulerpartlemt  34336  eulerpartgbij  34337  eulerpartlemmf  34340  eulerpartlemgvv  34341  eulerpartlemgf  34344  eulerpart  34347  sseqmw  34356  sseqf  34357  sseqp1  34360  fiblem  34363  fibp1  34366  dstrvprob  34436  coinflipspace  34445  coinfliprv  34447  coinflippv  34448  ballotlem1  34451  ballotlem8  34501  circlemethhgt  34620  usgrcyclgt2v  35099  iccllysconn  35218  rellysconn  35219  satf00  35342  fmla0  35350  msrid  35513  dfrdg2  35759  dfrdg4  35915  imagesset  35917  elhf  36138  filnetlem3  36346  limsucncmpi  36411  bj-babygodel  36569  bj-idres  37126  taupilem3  37285  icoreresf  37318  icoreelrnab  37320  relowlssretop  37329  poimirlem3  37583  poimirlem9  37589  poimirlem15  37595  poimirlem16  37596  poimirlem17  37597  poimirlem19  37599  poimirlem27  37607  poimirlem28  37608  poimirlem31  37611  poimirlem32  37612  mblfinlem1  37617  ovoliunnfl  37622  voliunnfl  37624  mbfresfi  37626  dvtan  37630  itg2addnc  37634  ftc1anclem3  37655  areacirc  37673  fdc  37705  ismrer1  37798  reheibor  37799  rngomndo  37895  gidsn  37912  ac6s6f  38133  eccnvepex  38291  cnvref4  38306  dfcnvrefrels2  38484  dfcnvrefrels3  38485  dedths  38918  tendo0co2  40745  erng1r  40952  dvalveclem  40982  dva0g  40984  dvh0g  41068  sn-it0e0  42391  sn-0tie0  42415  2rexfrabdioph  42752  3rexfrabdioph  42753  4rexfrabdioph  42754  6rexfrabdioph  42755  7rexfrabdioph  42756  rencldnfi  42777  jm2.27dlem2  42967  wepwso  43000  dfac11  43019  pwssplit4  43046  frlmpwfi  43055  isnumbasgrplem3  43062  mpaaeu  43107  proot1mul  43155  proot1hash  43156  epirron  43215  oneptr  43216  ordeldif1o  43222  oaomoencom  43279  oenassex  43280  cnvcnvintabd  43562  cnvrcl0  43587  dfrtrcl5  43591  cotrcltrcl  43687  frege92  43917  seff  44278  prmunb2  44280  binomcxplemdvbinom  44322  binomcxplemcvg  44323  binomcxplemnotnn0  44325  sumsnd  44926  islptre  45540  stoweidlem34  45955  stoweidlem37  45958  stirlinglem11  46005  stirlinglem12  46006  stirlinglem13  46007  fouriersw  46152  natlocalincr  46795  upwordsing  46803  fundcmpsurbijinjpreimafv  47281  fundcmpsurinjimaid  47285  fmtnoinf  47410  gbowge7  47637  nnsum3primes4  47662  usgrexmpl12ngrlic  47854  2zrng0  47967  lmodn0  48224  zlmodzxzldeplem3  48231  lvecpsslmod  48236  0dig2pr01  48344  aacllem  48895  amgmwlem  48896