Theorem ringmnd 20222

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

Syntax hints:   → wi 4   ∈ wcel 2119  Mndcmnd 18700  Ringcrg 20212

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-nul 5235

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-sbc 3731  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-iota 6448  df-fv 6500  df-ov 7366  df-grp 18910  df-ring 20214

This theorem is referenced by:  ringmgm  20223  gsummulc1  20293  gsummulc2  20294  gsummgp0  20295  prdsringd  20298  pwsco1rhm  20480  suborng  20855  lmodvsmmulgdi  20894  rngqiprngimf1  21300  cnfldmulg  21386  cnsubmlem  21397  gsumfsum  21416  nn0srg  21419  rge0srg  21420  zring0  21440  freshmansdream  21556  re0g  21594  uvcresum  21775  psrlidm  21943  psrridm  21944  mplsubrglem  21985  mplmonmul  22019  evlslem2  22062  evlslem3  22063  evlsgsumadd  22079  mhpmulcl  22144  coe1tmmul2  22269  coe1tmmul  22270  cply1mul  22289  gsummoncoe1  22301  evls1gsumadd  22317  mamudi  22393  mamudir  22394  mamulid  22431  mamurid  22432  mat1dimmul  22466  mat1mhm  22474  dmatmul  22487  scmatscm  22503  1mavmul  22538  mulmarep1gsum1  22563  mdet0pr  22582  m1detdiag  22587  mdetdiag  22589  mdet0  22596  m2detleib  22621  maducoeval2  22630  madugsum  22633  smadiadetlem1a  22653  smadiadetlem3  22658  smadiadet  22660  cpmatmcllem  22708  mat2pmatghm  22720  mat2pmatmul  22721  pmatcollpw3fi1lem1  22776  idpm2idmp  22791  mp2pm2mplem4  22799  pm2mpghm  22806  monmat2matmon  22814  pm2mp  22815  chfacfscmulgsum  22850  chfacfpmmulgsum  22854  cpmadugsumlemF  22866  cayhamlem4  22878  tdeglem4  26050  tdeglem2  26051  mdegmullem  26068  coe1mul3  26089  plypf1  26202  tayl0  26352  jensen  26977  amgmlem  26978  elrgspnlem1  33330  elrgspnlem3  33332  subrdom  33373  xrge0slmod  33438  ressply1invg  33659  psrmonmul  33741  esplyfval1  33764  drgext0gsca  33783  ply1degltdimlem  33813  fedgmullem2  33821  extdg1id  33857  evls1fldgencl  33861  zringnm  34149  rezh  34160  ringexp0nn  42626  aks6d1c6lem1  42662  amgm2d  44649  amgm3d  44650  amgm4d  44651  2zrng0  48742  cznrng  48759  mgpsumz  48860  ply1mulgsumlem2  48885  amgmwlem  50299  amgmw2d  50301