Theorem ringmnd 20215

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

Syntax hints:   → wi 4   ∈ wcel 2114  Mndcmnd 18693  Ringcrg 20205

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-nul 5241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6448  df-fv 6500  df-ov 7363  df-grp 18903  df-ring 20207

This theorem is referenced by:  ringmgm  20216  gsummulc1  20286  gsummulc2  20287  gsummgp0  20288  prdsringd  20291  pwsco1rhm  20470  suborng  20844  lmodvsmmulgdi  20883  rngqiprngimf1  21290  cnfldmulg  21393  cnsubmlem  21404  gsumfsum  21424  nn0srg  21427  rge0srg  21428  zring0  21448  freshmansdream  21564  re0g  21602  uvcresum  21783  psrlidm  21950  psrridm  21951  mplsubrglem  21992  mplmonmul  22024  evlslem2  22067  evlslem3  22068  evlsgsumadd  22084  mhpmulcl  22125  coe1tmmul2  22251  coe1tmmul  22252  cply1mul  22271  gsummoncoe1  22283  evls1gsumadd  22299  mamudi  22378  mamudir  22379  mamulid  22416  mamurid  22417  mat1dimmul  22451  mat1mhm  22459  dmatmul  22472  scmatscm  22488  1mavmul  22523  mulmarep1gsum1  22548  mdet0pr  22567  m1detdiag  22572  mdetdiag  22574  mdet0  22581  m2detleib  22606  maducoeval2  22615  madugsum  22618  smadiadetlem1a  22638  smadiadetlem3  22643  smadiadet  22645  cpmatmcllem  22693  mat2pmatghm  22705  mat2pmatmul  22706  pmatcollpw3fi1lem1  22761  idpm2idmp  22776  mp2pm2mplem4  22784  pm2mpghm  22791  monmat2matmon  22799  pm2mp  22800  chfacfscmulgsum  22835  chfacfpmmulgsum  22839  cpmadugsumlemF  22851  cayhamlem4  22863  tdeglem4  26035  tdeglem2  26036  mdegmullem  26053  coe1mul3  26074  plypf1  26187  tayl0  26338  jensen  26966  amgmlem  26967  elrgspnlem1  33318  elrgspnlem3  33320  subrdom  33361  xrge0slmod  33423  ressply1invg  33644  psrmonmul  33709  esplyfval1  33732  drgext0gsca  33751  ply1degltdimlem  33782  fedgmullem2  33790  extdg1id  33826  evls1fldgencl  33830  zringnm  34118  rezh  34129  ringexp0nn  42587  aks6d1c6lem1  42623  amgm2d  44643  amgm3d  44644  amgm4d  44645  2zrng0  48732  cznrng  48749  mgpsumz  48850  ply1mulgsumlem2  48875  amgmwlem  50289  amgmw2d  50291