Theorem ringmnd 19708

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

Syntax hints:   → wi 4   ∈ wcel 2108  Mndcmnd 18300  Ringcrg 19698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-nul 5225

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426  df-ov 7258  df-grp 18495  df-ring 19700

This theorem is referenced by:  ringmgm  19709  gsummulc1  19760  gsummulc2  19761  gsummgp0  19762  prdsringd  19766  pwsco1rhm  19897  lmodvsmmulgdi  20073  cnfldmulg  20542  cnsubmlem  20558  gsumfsum  20577  nn0srg  20580  rge0srg  20581  zring0  20592  re0g  20729  uvcresum  20910  psrlidm  21082  psrridm  21083  mplsubrglem  21120  mplmonmul  21147  evlslem2  21199  evlslem3  21200  evlsgsumadd  21211  mhpmulcl  21249  coe1tmmul2  21357  coe1tmmul  21358  cply1mul  21375  gsummoncoe1  21385  evls1gsumadd  21400  mamudi  21460  mamudir  21461  mamulid  21498  mamurid  21499  mat1dimmul  21533  mat1mhm  21541  dmatmul  21554  scmatscm  21570  1mavmul  21605  mulmarep1gsum1  21630  mdet0pr  21649  m1detdiag  21654  mdetdiag  21656  mdet0  21663  m2detleib  21688  maducoeval2  21697  madugsum  21700  smadiadetlem1a  21720  smadiadetlem3  21725  smadiadet  21727  cpmatmcllem  21775  mat2pmatghm  21787  mat2pmatmul  21788  pmatcollpw3fi1lem1  21843  idpm2idmp  21858  mp2pm2mplem4  21866  pm2mpghm  21873  monmat2matmon  21881  pm2mp  21882  chfacfscmulgsum  21917  chfacfpmmulgsum  21921  cpmadugsumlemF  21933  cayhamlem4  21945  tdeglem4  25129  tdeglem4OLD  25130  tdeglem2  25131  mdegmullem  25148  coe1mul3  25169  plypf1  25278  tayl0  25426  jensen  26043  amgmlem  26044  freshmansdream  31386  suborng  31416  xrge0slmod  31450  drgext0gsca  31581  fedgmullem2  31613  extdg1id  31640  zringnm  31810  rezh  31821  amgm2d  41698  amgm3d  41699  amgm4d  41700  2zrng0  45384  cznrng  45401  mgpsumz  45586  ply1mulgsumlem2  45616  amgmwlem  46392  amgmw2d  46394