Theorem ringmnd 20203

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

Syntax hints:   → wi 4   ∈ wcel 2108  Mndcmnd 18712  Ringcrg 20193

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-nul 5276

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-sbc 3766  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6484  df-fv 6539  df-ov 7408  df-grp 18919  df-ring 20195

This theorem is referenced by:  ringmgm  20204  gsummulc1OLD  20274  gsummulc2OLD  20275  gsummulc1  20276  gsummulc2  20277  gsummgp0  20278  prdsringd  20281  pwsco1rhm  20462  lmodvsmmulgdi  20854  rngqiprngimf1  21261  cnfldmulg  21366  cnsubmlem  21382  gsumfsum  21402  nn0srg  21405  rge0srg  21406  zring0  21419  freshmansdream  21535  re0g  21572  uvcresum  21753  psrlidm  21922  psrridm  21923  mplsubrglem  21964  mplmonmul  21994  evlslem2  22037  evlslem3  22038  evlsgsumadd  22049  mhpmulcl  22087  coe1tmmul2  22213  coe1tmmul  22214  cply1mul  22234  gsummoncoe1  22246  evls1gsumadd  22262  mamudi  22341  mamudir  22342  mamulid  22379  mamurid  22380  mat1dimmul  22414  mat1mhm  22422  dmatmul  22435  scmatscm  22451  1mavmul  22486  mulmarep1gsum1  22511  mdet0pr  22530  m1detdiag  22535  mdetdiag  22537  mdet0  22544  m2detleib  22569  maducoeval2  22578  madugsum  22581  smadiadetlem1a  22601  smadiadetlem3  22606  smadiadet  22608  cpmatmcllem  22656  mat2pmatghm  22668  mat2pmatmul  22669  pmatcollpw3fi1lem1  22724  idpm2idmp  22739  mp2pm2mplem4  22747  pm2mpghm  22754  monmat2matmon  22762  pm2mp  22763  chfacfscmulgsum  22798  chfacfpmmulgsum  22802  cpmadugsumlemF  22814  cayhamlem4  22826  tdeglem4  26017  tdeglem2  26018  mdegmullem  26035  coe1mul3  26056  plypf1  26169  tayl0  26321  jensen  26951  amgmlem  26952  elrgspnlem1  33237  elrgspnlem3  33239  subrdom  33279  suborng  33337  xrge0slmod  33363  ressply1invg  33582  drgext0gsca  33631  ply1degltdimlem  33662  fedgmullem2  33670  extdg1id  33707  evls1fldgencl  33711  zringnm  33989  rezh  34000  ringexp0nn  42147  aks6d1c6lem1  42183  amgm2d  44222  amgm3d  44223  amgm4d  44224  2zrng0  48219  cznrng  48236  mgpsumz  48337  ply1mulgsumlem2  48363  amgmwlem  49666  amgmw2d  49668