Theorem ringmnd 19888

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

Syntax hints:   → wi 4   ∈ wcel 2105  Mndcmnd 18482  Ringcrg 19878

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707  ax-nul 5250

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3443  df-sbc 3728  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4270  df-if 4474  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4853  df-br 5093  df-iota 6431  df-fv 6487  df-ov 7340  df-grp 18676  df-ring 19880

This theorem is referenced by:  ringmgm  19889  gsummulc1  19940  gsummulc2  19941  gsummgp0  19942  prdsringd  19946  pwsco1rhm  20080  lmodvsmmulgdi  20264  cnfldmulg  20736  cnsubmlem  20752  gsumfsum  20771  nn0srg  20774  rge0srg  20775  zring0  20786  re0g  20923  uvcresum  21106  psrlidm  21278  psrridm  21279  mplsubrglem  21316  mplmonmul  21343  evlslem2  21395  evlslem3  21396  evlsgsumadd  21407  mhpmulcl  21445  coe1tmmul2  21553  coe1tmmul  21554  cply1mul  21571  gsummoncoe1  21581  evls1gsumadd  21596  mamudi  21656  mamudir  21657  mamulid  21696  mamurid  21697  mat1dimmul  21731  mat1mhm  21739  dmatmul  21752  scmatscm  21768  1mavmul  21803  mulmarep1gsum1  21828  mdet0pr  21847  m1detdiag  21852  mdetdiag  21854  mdet0  21861  m2detleib  21886  maducoeval2  21895  madugsum  21898  smadiadetlem1a  21918  smadiadetlem3  21923  smadiadet  21925  cpmatmcllem  21973  mat2pmatghm  21985  mat2pmatmul  21986  pmatcollpw3fi1lem1  22041  idpm2idmp  22056  mp2pm2mplem4  22064  pm2mpghm  22071  monmat2matmon  22079  pm2mp  22080  chfacfscmulgsum  22115  chfacfpmmulgsum  22119  cpmadugsumlemF  22131  cayhamlem4  22143  tdeglem4  25330  tdeglem4OLD  25331  tdeglem2  25332  mdegmullem  25349  coe1mul3  25370  plypf1  25479  tayl0  25627  jensen  26244  amgmlem  26245  freshmansdream  31771  suborng  31814  xrge0slmod  31844  drgext0gsca  31977  fedgmullem2  32009  extdg1id  32036  zringnm  32206  rezh  32219  amgm2d  42139  amgm3d  42140  amgm4d  42141  2zrng0  45856  cznrng  45873  mgpsumz  46058  ply1mulgsumlem2  46088  amgmwlem  46866  amgmw2d  46868