Theorem ringmnd 20159

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

Syntax hints:   → wi 4   ∈ wcel 2109  Mndcmnd 18668  Ringcrg 20149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-nul 5264

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393  df-grp 18875  df-ring 20151

This theorem is referenced by:  ringmgm  20160  gsummulc1OLD  20230  gsummulc2OLD  20231  gsummulc1  20232  gsummulc2  20233  gsummgp0  20234  prdsringd  20237  pwsco1rhm  20418  lmodvsmmulgdi  20810  rngqiprngimf1  21217  cnfldmulg  21322  cnsubmlem  21338  gsumfsum  21358  nn0srg  21361  rge0srg  21362  zring0  21375  freshmansdream  21491  re0g  21528  uvcresum  21709  psrlidm  21878  psrridm  21879  mplsubrglem  21920  mplmonmul  21950  evlslem2  21993  evlslem3  21994  evlsgsumadd  22005  mhpmulcl  22043  coe1tmmul2  22169  coe1tmmul  22170  cply1mul  22190  gsummoncoe1  22202  evls1gsumadd  22218  mamudi  22297  mamudir  22298  mamulid  22335  mamurid  22336  mat1dimmul  22370  mat1mhm  22378  dmatmul  22391  scmatscm  22407  1mavmul  22442  mulmarep1gsum1  22467  mdet0pr  22486  m1detdiag  22491  mdetdiag  22493  mdet0  22500  m2detleib  22525  maducoeval2  22534  madugsum  22537  smadiadetlem1a  22557  smadiadetlem3  22562  smadiadet  22564  cpmatmcllem  22612  mat2pmatghm  22624  mat2pmatmul  22625  pmatcollpw3fi1lem1  22680  idpm2idmp  22695  mp2pm2mplem4  22703  pm2mpghm  22710  monmat2matmon  22718  pm2mp  22719  chfacfscmulgsum  22754  chfacfpmmulgsum  22758  cpmadugsumlemF  22770  cayhamlem4  22782  tdeglem4  25972  tdeglem2  25973  mdegmullem  25990  coe1mul3  26011  plypf1  26124  tayl0  26276  jensen  26906  amgmlem  26907  elrgspnlem1  33200  elrgspnlem3  33202  subrdom  33242  suborng  33300  xrge0slmod  33326  ressply1invg  33545  drgext0gsca  33594  ply1degltdimlem  33625  fedgmullem2  33633  extdg1id  33668  evls1fldgencl  33672  zringnm  33955  rezh  33966  ringexp0nn  42129  aks6d1c6lem1  42165  amgm2d  44194  amgm3d  44195  amgm4d  44196  2zrng0  48236  cznrng  48253  mgpsumz  48354  ply1mulgsumlem2  48380  amgmwlem  49795  amgmw2d  49797