Theorem ringmnd 20316

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

Syntax hints:   → wi 4   ∈ wcel 2145  Mndcmnd 18782  Ringcrg 20306

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-nul 5261

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-sbc 3748  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-iota 6481  df-fv 6533  df-ov 7403  df-grp 18993  df-ring 20308

This theorem is referenced by:  ringmgm  20317  gsummulc1  20388  gsummulc2  20389  gsummgp0  20390  prdsringd  20393  pwsco1rhm  20575  suborng  20948  lmodvsmmulgdi  20987  rngqiprngimf1  21402  cnfldmulg  21514  cnsubmlem  21525  gsumfsum  21544  nn0srg  21547  rge0srg  21548  zring0  21568  freshmansdream  21684  re0g  21722  uvcresum  21903  psrlidm  22071  psrridm  22072  mplsubrglem  22113  mplmonmul  22147  evlslem2  22190  evlslem3  22191  evlsgsumadd  22207  mhpmulcl  22272  coe1tmmul2  22397  coe1tmmul  22398  cply1mul  22417  gsummoncoe1  22429  evls1gsumadd  22445  mamudi  22521  mamudir  22522  mamulid  22559  mamurid  22560  mat1dimmul  22594  mat1mhm  22602  dmatmul  22615  scmatscm  22631  1mavmul  22666  mulmarep1gsum1  22691  mdet0pr  22710  m1detdiag  22715  mdetdiag  22717  mdet0  22724  m2detleib  22749  maducoeval2  22758  madugsum  22761  smadiadetlem1a  22781  smadiadetlem3  22786  smadiadet  22788  cpmatmcllem  22836  mat2pmatghm  22848  mat2pmatmul  22849  pmatcollpw3fi1lem1  22904  idpm2idmp  22919  mp2pm2mplem4  22927  pm2mpghm  22934  monmat2matmon  22942  pm2mp  22943  chfacfscmulgsum  22978  chfacfpmmulgsum  22982  cpmadugsumlemF  22994  cayhamlem4  23006  tdeglem4  26178  tdeglem2  26179  mdegmullem  26196  coe1mul3  26217  plypf1  26330  tayl0  26483  jensen  27111  amgmlem  27112  elrgspnlem1  33475  elrgspnlem3  33477  subrdom  33518  xrge0slmod  33583  ressply1invg  33776  psrmonmul  33857  esplyfval1  33880  drgext0gsca  33899  ply1degltdimlem  33929  fedgmullem2  33937  extdg1id  33973  evls1fldgencl  33977  zringnm  34265  rezh  34276  ringexp0nn  42763  aks6d1c6lem1  42799  amgm2d  44786  amgm3d  44787  amgm4d  44788  2zrng0  48864  cznrng  48881  mgpsumz  48993  ply1mulgsumlem2  49018  amgmwlem  50431  amgmw2d  50433