Theorem ringmnd 20475

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  Mndcmnd 18928  Ringcrg 20464

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-nul 5259

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546  df-ov 7423  df-grp 19152  df-ring 20466

This theorem is used by:  ringmgm  20476  gsummulc1  20550  gsummulc2  20551  gsummgp0  20552  prdsringd  20555  pwsco1rhm  20746  suborng  21138  lmodvsmmulgdi  21177  rngqiprngimf1  21601  cnfldmulg  21715  cnsubmlem  21726  gsumfsum  21745  nn0srg  21748  rge0srg  21749  zring0  21769  freshmansdream  21885  re0g  21923  uvcresum  22104  psrlidm  22274  psrridm  22275  mplsubrglem  22316  mplmonmul  22350  evlslem2  22393  evlslem3  22394  evlsgsumadd  22410  mhpmulcl  22475  coe1tmmul2  22600  coe1tmmul  22601  cply1mul  22619  gsummoncoe1  22631  evls1gsumadd  22647  mamudi  22723  mamudir  22724  mamulid  22761  mamurid  22762  mat1dimmul  22796  mat1mhm  22804  dmatmul  22817  scmatscm  22833  1mavmul  22868  mulmarep1gsum1  22893  mdet0pr  22912  m1detdiag  22917  mdetdiag  22919  mdet0  22926  m2detleib  22951  maducoeval2  22960  madugsum  22963  smadiadetlem1a  22983  smadiadetlem3  22988  smadiadet  22990  cpmatmcllem  23041  mat2pmatghm  23053  mat2pmatmul  23054  pmatcollpw3fi1lem1  23109  idpm2idmp  23124  mp2pm2mplem4  23132  pm2mpghm  23139  monmat2matmon  23147  pm2mp  23148  chfacfscmulgsum  23183  chfacfpmmulgsum  23187  cpmadugsumlemF  23199  cayhamlem4  23211  tdeglem4  26383  tdeglem2  26384  mdegmullem  26401  coe1mul3  26422  plypf1  26536  tayl0  26694  jensen  27321  amgmlem  27322  elrgspnlem1  33849  elrgspnlem3  33851  subrdom  33892  xrge0slmod  33955  ressply1invg  34147  psrmonmul  34228  esplyfval1  34251  drgext0gsca  34270  ply1degltdimlem  34300  fedgmullem2  34308  extdg1id  34344  evls1fldgencl  34348  zringnm  34636  rezh  34647  ringexp0nn  43277  aks6d1c6lem1  43313  amgm2d  45291  amgm3d  45292  amgm4d  45293  2zrng0  49434  cznrng  49451  mgpsumz  49567  ply1mulgsumlem2  49592  amgmwlem  51155  amgmw2d  51157