Theorem ringmnd 20137

Description: A ring is a monoid under addition. (Contributed by Mario Carneiro, 7-Jan-2015.)

Assertion

Ref	Expression
ringmnd	⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd)

Proof of Theorem ringmnd

Step	Hyp	Ref	Expression
1		ringgrp 20132	. 2 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)
2	1	grpmndd 18868	1 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd)

Syntax hints:   → wi 4   ∈ wcel 2106  Mndcmnd 18659  Ringcrg 20127

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-nul 5306

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3778  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551  df-ov 7414  df-grp 18858  df-ring 20129

This theorem is referenced by:  ringmgm  20138  gsummulc1OLD  20202  gsummulc2OLD  20203  gsummulc1  20204  gsummulc2  20205  gsummgp0  20206  prdsringd  20209  pwsco1rhm  20393  lmodvsmmulgdi  20651  rngqiprngimf1  21059  cnfldmulg  21177  cnsubmlem  21193  gsumfsum  21212  nn0srg  21215  rge0srg  21216  zring0  21229  re0g  21384  uvcresum  21567  psrlidm  21742  psrridm  21743  mplsubrglem  21782  mplmonmul  21810  evlslem2  21861  evlslem3  21862  evlsgsumadd  21873  mhpmulcl  21911  coe1tmmul2  22018  coe1tmmul  22019  cply1mul  22038  gsummoncoe1  22048  evls1gsumadd  22063  mamudi  22123  mamudir  22124  mamulid  22163  mamurid  22164  mat1dimmul  22198  mat1mhm  22206  dmatmul  22219  scmatscm  22235  1mavmul  22270  mulmarep1gsum1  22295  mdet0pr  22314  m1detdiag  22319  mdetdiag  22321  mdet0  22328  m2detleib  22353  maducoeval2  22362  madugsum  22365  smadiadetlem1a  22385  smadiadetlem3  22390  smadiadet  22392  cpmatmcllem  22440  mat2pmatghm  22452  mat2pmatmul  22453  pmatcollpw3fi1lem1  22508  idpm2idmp  22523  mp2pm2mplem4  22531  pm2mpghm  22538  monmat2matmon  22546  pm2mp  22547  chfacfscmulgsum  22582  chfacfpmmulgsum  22586  cpmadugsumlemF  22598  cayhamlem4  22610  tdeglem4  25801  tdeglem4OLD  25802  tdeglem2  25803  mdegmullem  25820  coe1mul3  25841  plypf1  25950  tayl0  26098  jensen  26717  amgmlem  26718  freshmansdream  32639  suborng  32691  xrge0slmod  32721  ressply1invg  32920  drgext0gsca  32954  ply1degltdimlem  32983  fedgmullem2  32991  extdg1id  33018  evls1fldgencl  33021  zringnm  33224  rezh  33237  amgm2d  43252  amgm3d  43253  amgm4d  43254  2zrng0  46925  cznrng  46942  mgpsumz  47127  ply1mulgsumlem2  47156  amgmwlem  47937  amgmw2d  47939