Theorem ringmnd 20240

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

Syntax hints:   → wi 4   ∈ wcel 2108  Mndcmnd 18747  Ringcrg 20230

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-nul 5306

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434  df-grp 18954  df-ring 20232

This theorem is referenced by:  ringmgm  20241  gsummulc1OLD  20311  gsummulc2OLD  20312  gsummulc1  20313  gsummulc2  20314  gsummgp0  20315  prdsringd  20318  pwsco1rhm  20502  lmodvsmmulgdi  20895  rngqiprngimf1  21310  cnfldmulg  21416  cnsubmlem  21432  gsumfsum  21452  nn0srg  21455  rge0srg  21456  zring0  21469  freshmansdream  21593  re0g  21630  uvcresum  21813  psrlidm  21982  psrridm  21983  mplsubrglem  22024  mplmonmul  22054  evlslem2  22103  evlslem3  22104  evlsgsumadd  22115  mhpmulcl  22153  coe1tmmul2  22279  coe1tmmul  22280  cply1mul  22300  gsummoncoe1  22312  evls1gsumadd  22328  mamudi  22407  mamudir  22408  mamulid  22447  mamurid  22448  mat1dimmul  22482  mat1mhm  22490  dmatmul  22503  scmatscm  22519  1mavmul  22554  mulmarep1gsum1  22579  mdet0pr  22598  m1detdiag  22603  mdetdiag  22605  mdet0  22612  m2detleib  22637  maducoeval2  22646  madugsum  22649  smadiadetlem1a  22669  smadiadetlem3  22674  smadiadet  22676  cpmatmcllem  22724  mat2pmatghm  22736  mat2pmatmul  22737  pmatcollpw3fi1lem1  22792  idpm2idmp  22807  mp2pm2mplem4  22815  pm2mpghm  22822  monmat2matmon  22830  pm2mp  22831  chfacfscmulgsum  22866  chfacfpmmulgsum  22870  cpmadugsumlemF  22882  cayhamlem4  22894  tdeglem4  26099  tdeglem2  26100  mdegmullem  26117  coe1mul3  26138  plypf1  26251  tayl0  26403  jensen  27032  amgmlem  27033  elrgspnlem1  33246  elrgspnlem3  33248  subrdom  33288  suborng  33345  xrge0slmod  33376  ressply1invg  33594  drgext0gsca  33642  ply1degltdimlem  33673  fedgmullem2  33681  extdg1id  33716  evls1fldgencl  33720  zringnm  33957  rezh  33970  ringexp0nn  42135  aks6d1c6lem1  42171  amgm2d  44211  amgm3d  44212  amgm4d  44213  2zrng0  48160  cznrng  48177  mgpsumz  48278  ply1mulgsumlem2  48304  amgmwlem  49321  amgmw2d  49323