Theorem ringmnd 20162

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

Syntax hints:   → wi 4   ∈ wcel 2111  Mndcmnd 18642  Ringcrg 20152

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 2113  ax-9 2121  ax-ext 2703  ax-nul 5244

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 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3742  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-iota 6437  df-fv 6489  df-ov 7349  df-grp 18849  df-ring 20154

This theorem is referenced by:  ringmgm  20163  gsummulc1OLD  20233  gsummulc2OLD  20234  gsummulc1  20235  gsummulc2  20236  gsummgp0  20237  prdsringd  20240  pwsco1rhm  20418  suborng  20792  lmodvsmmulgdi  20831  rngqiprngimf1  21238  cnfldmulg  21341  cnsubmlem  21352  gsumfsum  21372  nn0srg  21375  rge0srg  21376  zring0  21396  freshmansdream  21512  re0g  21550  uvcresum  21731  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  33207  elrgspnlem3  33209  subrdom  33249  xrge0slmod  33311  ressply1invg  33530  drgext0gsca  33602  ply1degltdimlem  33633  fedgmullem2  33641  extdg1id  33677  evls1fldgencl  33681  zringnm  33969  rezh  33980  ringexp0nn  42173  aks6d1c6lem1  42209  amgm2d  44237  amgm3d  44238  amgm4d  44239  2zrng0  48281  cznrng  48298  mgpsumz  48399  ply1mulgsumlem2  48425  amgmwlem  49840  amgmw2d  49842