Theorem ringmnd 20161

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

Syntax hints:   → wi 4   ∈ wcel 2111  Mndcmnd 18642  Ringcrg 20151

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 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-nul 5242

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3737  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-iota 6437  df-fv 6489  df-ov 7349  df-grp 18849  df-ring 20153

This theorem is referenced by:  ringmgm  20162  gsummulc1OLD  20232  gsummulc2OLD  20233  gsummulc1  20234  gsummulc2  20235  gsummgp0  20236  prdsringd  20239  pwsco1rhm  20417  suborng  20791  lmodvsmmulgdi  20830  rngqiprngimf1  21237  cnfldmulg  21340  cnsubmlem  21351  gsumfsum  21371  nn0srg  21374  rge0srg  21375  zring0  21395  freshmansdream  21511  re0g  21549  uvcresum  21730  psrlidm  21899  psrridm  21900  mplsubrglem  21941  mplmonmul  21971  evlslem2  22014  evlslem3  22015  evlsgsumadd  22026  mhpmulcl  22064  coe1tmmul2  22190  coe1tmmul  22191  cply1mul  22211  gsummoncoe1  22223  evls1gsumadd  22239  mamudi  22318  mamudir  22319  mamulid  22356  mamurid  22357  mat1dimmul  22391  mat1mhm  22399  dmatmul  22412  scmatscm  22428  1mavmul  22463  mulmarep1gsum1  22488  mdet0pr  22507  m1detdiag  22512  mdetdiag  22514  mdet0  22521  m2detleib  22546  maducoeval2  22555  madugsum  22558  smadiadetlem1a  22578  smadiadetlem3  22583  smadiadet  22585  cpmatmcllem  22633  mat2pmatghm  22645  mat2pmatmul  22646  pmatcollpw3fi1lem1  22701  idpm2idmp  22716  mp2pm2mplem4  22724  pm2mpghm  22731  monmat2matmon  22739  pm2mp  22740  chfacfscmulgsum  22775  chfacfpmmulgsum  22779  cpmadugsumlemF  22791  cayhamlem4  22803  tdeglem4  25992  tdeglem2  25993  mdegmullem  26010  coe1mul3  26031  plypf1  26144  tayl0  26296  jensen  26926  amgmlem  26927  elrgspnlem1  33209  elrgspnlem3  33211  subrdom  33251  xrge0slmod  33313  ressply1invg  33532  drgext0gsca  33604  ply1degltdimlem  33635  fedgmullem2  33643  extdg1id  33679  evls1fldgencl  33683  zringnm  33971  rezh  33982  ringexp0nn  42226  aks6d1c6lem1  42262  amgm2d  44290  amgm3d  44291  amgm4d  44292  2zrng0  48343  cznrng  48360  mgpsumz  48461  ply1mulgsumlem2  48487  amgmwlem  49902  amgmw2d  49904