Theorem ringmnd 20272

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 20267	. 2 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)
2	1	grpmndd 18971	1 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd)

Syntax hints:   → wi 4   ∈ wcel 2141  Mndcmnd 18751  Ringcrg 20262

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-nul 5255

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-sbc 3745  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-iota 6473  df-fv 6525  df-ov 7395  df-grp 18961  df-ring 20264

This theorem is referenced by:  ringmgm  20273  gsummulc1  20343  gsummulc2  20344  gsummgp0  20345  prdsringd  20348  pwsco1rhm  20530  suborng  20905  lmodvsmmulgdi  20944  rngqiprngimf1  21350  cnfldmulg  21436  cnsubmlem  21447  gsumfsum  21466  nn0srg  21469  rge0srg  21470  zring0  21490  freshmansdream  21606  re0g  21644  uvcresum  21825  psrlidm  21993  psrridm  21994  mplsubrglem  22035  mplmonmul  22069  evlslem2  22112  evlslem3  22113  evlsgsumadd  22129  mhpmulcl  22194  coe1tmmul2  22319  coe1tmmul  22320  cply1mul  22339  gsummoncoe1  22351  evls1gsumadd  22367  mamudi  22443  mamudir  22444  mamulid  22481  mamurid  22482  mat1dimmul  22516  mat1mhm  22524  dmatmul  22537  scmatscm  22553  1mavmul  22588  mulmarep1gsum1  22613  mdet0pr  22632  m1detdiag  22637  mdetdiag  22639  mdet0  22646  m2detleib  22671  maducoeval2  22680  madugsum  22683  smadiadetlem1a  22703  smadiadetlem3  22708  smadiadet  22710  cpmatmcllem  22758  mat2pmatghm  22770  mat2pmatmul  22771  pmatcollpw3fi1lem1  22826  idpm2idmp  22841  mp2pm2mplem4  22849  pm2mpghm  22856  monmat2matmon  22864  pm2mp  22865  chfacfscmulgsum  22900  chfacfpmmulgsum  22904  cpmadugsumlemF  22916  cayhamlem4  22928  tdeglem4  26100  tdeglem2  26101  mdegmullem  26118  coe1mul3  26139  plypf1  26252  tayl0  26402  jensen  27030  amgmlem  27031  elrgspnlem1  33384  elrgspnlem3  33386  subrdom  33430  xrge0slmod  33495  ressply1invg  33726  psrmonmul  33808  esplyfval1  33831  drgext0gsca  33850  ply1degltdimlem  33880  fedgmullem2  33888  extdg1id  33924  evls1fldgencl  33928  zringnm  34216  rezh  34227  ringexp0nn  42715  aks6d1c6lem1  42751  amgm2d  44738  amgm3d  44739  amgm4d  44740  2zrng0  48830  cznrng  48847  mgpsumz  48948  ply1mulgsumlem2  48973  amgmwlem  50387  amgmw2d  50389