Theorem ringmnd 20388

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Mndcmnd 18842  Ringcrg 20378

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-nul 5267

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-sbc 3743  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-ov 7420  df-grp 19066  df-ring 20380

This theorem is used by:  ringmgm  20389  gsummulc1  20462  gsummulc2  20463  gsummgp0  20464  prdsringd  20467  pwsco1rhm  20658  suborng  21048  lmodvsmmulgdi  21087  rngqiprngimf1  21509  cnfldmulg  21623  cnsubmlem  21634  gsumfsum  21653  nn0srg  21656  rge0srg  21657  zring0  21677  freshmansdream  21793  re0g  21831  uvcresum  22012  psrlidm  22182  psrridm  22183  mplsubrglem  22224  mplmonmul  22258  evlslem2  22301  evlslem3  22302  evlsgsumadd  22318  mhpmulcl  22383  coe1tmmul2  22508  coe1tmmul  22509  cply1mul  22527  gsummoncoe1  22539  evls1gsumadd  22555  mamudi  22631  mamudir  22632  mamulid  22669  mamurid  22670  mat1dimmul  22704  mat1mhm  22712  dmatmul  22725  scmatscm  22741  1mavmul  22776  mulmarep1gsum1  22801  mdet0pr  22820  m1detdiag  22825  mdetdiag  22827  mdet0  22834  m2detleib  22859  maducoeval2  22868  madugsum  22871  smadiadetlem1a  22891  smadiadetlem3  22896  smadiadet  22898  cpmatmcllem  22949  mat2pmatghm  22961  mat2pmatmul  22962  pmatcollpw3fi1lem1  23017  idpm2idmp  23032  mp2pm2mplem4  23040  pm2mpghm  23047  monmat2matmon  23055  pm2mp  23056  chfacfscmulgsum  23091  chfacfpmmulgsum  23095  cpmadugsumlemF  23107  cayhamlem4  23119  tdeglem4  26292  tdeglem2  26293  mdegmullem  26310  coe1mul3  26331  plypf1  26445  tayl0  26605  jensen  27233  amgmlem  27234  elrgspnlem1  33690  elrgspnlem3  33692  subrdom  33733  xrge0slmod  33796  ressply1invg  33987  psrmonmul  34068  esplyfval1  34091  drgext0gsca  34110  ply1degltdimlem  34140  fedgmullem2  34148  extdg1id  34184  evls1fldgencl  34188  zringnm  34476  rezh  34487  ringexp0nn  43008  aks6d1c6lem1  43044  amgm2d  45046  amgm3d  45047  amgm4d  45048  2zrng0  49167  cznrng  49184  mgpsumz  49300  ply1mulgsumlem2  49325  amgmwlem  50828  amgmw2d  50830