Theorem ringmnd 20326

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

Syntax hints:   → wi 4   ∈ wcel 2143  Mndcmnd 18793  Ringcrg 20316

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-nul 5270

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3746  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-iota 6494  df-fv 6546  df-ov 7415  df-grp 19004  df-ring 20318

This theorem is referenced by:  ringmgm  20327  gsummulc1  20398  gsummulc2  20399  gsummgp0  20400  prdsringd  20403  pwsco1rhm  20585  suborng  20960  lmodvsmmulgdi  20999  rngqiprngimf1  21421  cnfldmulg  21535  cnsubmlem  21546  gsumfsum  21565  nn0srg  21568  rge0srg  21569  zring0  21589  freshmansdream  21705  re0g  21743  uvcresum  21924  psrlidm  22092  psrridm  22093  mplsubrglem  22134  mplmonmul  22168  evlslem2  22211  evlslem3  22212  evlsgsumadd  22228  mhpmulcl  22293  coe1tmmul2  22418  coe1tmmul  22419  cply1mul  22437  gsummoncoe1  22449  evls1gsumadd  22465  mamudi  22541  mamudir  22542  mamulid  22579  mamurid  22580  mat1dimmul  22614  mat1mhm  22622  dmatmul  22635  scmatscm  22651  1mavmul  22686  mulmarep1gsum1  22711  mdet0pr  22730  m1detdiag  22735  mdetdiag  22737  mdet0  22744  m2detleib  22769  maducoeval2  22778  madugsum  22781  smadiadetlem1a  22801  smadiadetlem3  22806  smadiadet  22808  cpmatmcllem  22856  mat2pmatghm  22868  mat2pmatmul  22869  pmatcollpw3fi1lem1  22924  idpm2idmp  22939  mp2pm2mplem4  22947  pm2mpghm  22954  monmat2matmon  22962  pm2mp  22963  chfacfscmulgsum  22998  chfacfpmmulgsum  23002  cpmadugsumlemF  23014  cayhamlem4  23026  tdeglem4  26198  tdeglem2  26199  mdegmullem  26216  coe1mul3  26237  plypf1  26350  tayl0  26503  jensen  27131  amgmlem  27132  elrgspnlem1  33540  elrgspnlem3  33542  subrdom  33583  xrge0slmod  33646  ressply1invg  33837  psrmonmul  33918  esplyfval1  33941  drgext0gsca  33960  ply1degltdimlem  33990  fedgmullem2  33998  extdg1id  34034  evls1fldgencl  34038  zringnm  34326  rezh  34337  ringexp0nn  42879  aks6d1c6lem1  42915  amgm2d  44904  amgm3d  44905  amgm4d  44906  2zrng0  48986  cznrng  49003  mgpsumz  49119  ply1mulgsumlem2  49144  amgmwlem  50579  amgmw2d  50581