Theorem ringmnd 20163

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

Syntax hints:   → wi 4   ∈ wcel 2113  Mndcmnd 18644  Ringcrg 20153

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-nul 5246

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2930  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-sbc 3738  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-iota 6442  df-fv 6494  df-ov 7355  df-grp 18851  df-ring 20155

This theorem is referenced by:  ringmgm  20164  gsummulc1OLD  20234  gsummulc2OLD  20235  gsummulc1  20236  gsummulc2  20237  gsummgp0  20238  prdsringd  20241  pwsco1rhm  20419  suborng  20793  lmodvsmmulgdi  20832  rngqiprngimf1  21239  cnfldmulg  21342  cnsubmlem  21353  gsumfsum  21373  nn0srg  21376  rge0srg  21377  zring0  21397  freshmansdream  21513  re0g  21551  uvcresum  21732  psrlidm  21900  psrridm  21901  mplsubrglem  21942  mplmonmul  21972  evlslem2  22015  evlslem3  22016  evlsgsumadd  22027  mhpmulcl  22065  coe1tmmul2  22191  coe1tmmul  22192  cply1mul  22212  gsummoncoe1  22224  evls1gsumadd  22240  mamudi  22319  mamudir  22320  mamulid  22357  mamurid  22358  mat1dimmul  22392  mat1mhm  22400  dmatmul  22413  scmatscm  22429  1mavmul  22464  mulmarep1gsum1  22489  mdet0pr  22508  m1detdiag  22513  mdetdiag  22515  mdet0  22522  m2detleib  22547  maducoeval2  22556  madugsum  22559  smadiadetlem1a  22579  smadiadetlem3  22584  smadiadet  22586  cpmatmcllem  22634  mat2pmatghm  22646  mat2pmatmul  22647  pmatcollpw3fi1lem1  22702  idpm2idmp  22717  mp2pm2mplem4  22725  pm2mpghm  22732  monmat2matmon  22740  pm2mp  22741  chfacfscmulgsum  22776  chfacfpmmulgsum  22780  cpmadugsumlemF  22792  cayhamlem4  22804  tdeglem4  25993  tdeglem2  25994  mdegmullem  26011  coe1mul3  26032  plypf1  26145  tayl0  26297  jensen  26927  amgmlem  26928  elrgspnlem1  33216  elrgspnlem3  33218  subrdom  33258  xrge0slmod  33320  ressply1invg  33539  drgext0gsca  33625  ply1degltdimlem  33656  fedgmullem2  33664  extdg1id  33700  evls1fldgencl  33704  zringnm  33992  rezh  34003  ringexp0nn  42248  aks6d1c6lem1  42284  amgm2d  44316  amgm3d  44317  amgm4d  44318  2zrng0  48369  cznrng  48386  mgpsumz  48487  ply1mulgsumlem2  48513  amgmwlem  49928  amgmw2d  49930