Theorem ringmnd 20066

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

Syntax hints:   → wi 4   ∈ wcel 2107  Mndcmnd 18625  Ringcrg 20056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-nul 5307

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3779  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412  df-grp 18822  df-ring 20058

This theorem is referenced by:  ringmgm  20067  gsummulc1OLD  20126  gsummulc2OLD  20127  gsummulc1  20128  gsummulc2  20129  gsummgp0  20130  prdsringd  20134  pwsco1rhm  20277  lmodvsmmulgdi  20507  cnfldmulg  20977  cnsubmlem  20993  gsumfsum  21012  nn0srg  21015  rge0srg  21016  zring0  21028  re0g  21165  uvcresum  21348  psrlidm  21523  psrridm  21524  mplsubrglem  21563  mplmonmul  21591  evlslem2  21642  evlslem3  21643  evlsgsumadd  21654  mhpmulcl  21692  coe1tmmul2  21798  coe1tmmul  21799  cply1mul  21818  gsummoncoe1  21828  evls1gsumadd  21843  mamudi  21903  mamudir  21904  mamulid  21943  mamurid  21944  mat1dimmul  21978  mat1mhm  21986  dmatmul  21999  scmatscm  22015  1mavmul  22050  mulmarep1gsum1  22075  mdet0pr  22094  m1detdiag  22099  mdetdiag  22101  mdet0  22108  m2detleib  22133  maducoeval2  22142  madugsum  22145  smadiadetlem1a  22165  smadiadetlem3  22170  smadiadet  22172  cpmatmcllem  22220  mat2pmatghm  22232  mat2pmatmul  22233  pmatcollpw3fi1lem1  22288  idpm2idmp  22303  mp2pm2mplem4  22311  pm2mpghm  22318  monmat2matmon  22326  pm2mp  22327  chfacfscmulgsum  22362  chfacfpmmulgsum  22366  cpmadugsumlemF  22378  cayhamlem4  22390  tdeglem4  25577  tdeglem4OLD  25578  tdeglem2  25579  mdegmullem  25596  coe1mul3  25617  plypf1  25726  tayl0  25874  jensen  26493  amgmlem  26494  freshmansdream  32412  suborng  32464  xrge0slmod  32494  ressply1invg  32689  drgext0gsca  32710  ply1degltdimlem  32738  fedgmullem2  32746  extdg1id  32773  zringnm  32969  rezh  32982  amgm2d  42998  amgm3d  42999  amgm4d  43000  rngqiprngimf1  46833  2zrng0  46884  cznrng  46901  mgpsumz  47086  ply1mulgsumlem2  47116  amgmwlem  47897  amgmw2d  47899