Theorem ringmnd 20220

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

Syntax hints:   → wi 4   ∈ wcel 2099  Mndcmnd 18720  Ringcrg 20210

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697  ax-nul 5302

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-ne 2931  df-ral 3052  df-rex 3061  df-rab 3421  df-v 3465  df-sbc 3777  df-dif 3950  df-un 3952  df-ss 3964  df-nul 4324  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4907  df-br 5145  df-iota 6496  df-fv 6552  df-ov 7417  df-grp 18924  df-ring 20212

This theorem is referenced by:  ringmgm  20221  gsummulc1OLD  20287  gsummulc2OLD  20288  gsummulc1  20289  gsummulc2  20290  gsummgp0  20291  prdsringd  20294  pwsco1rhm  20478  lmodvsmmulgdi  20867  rngqiprngimf1  21283  cnfldmulg  21389  cnsubmlem  21405  gsumfsum  21425  nn0srg  21428  rge0srg  21429  zring0  21442  freshmansdream  21566  re0g  21602  uvcresum  21785  psrlidm  21965  psrridm  21966  mplsubrglem  22007  mplmonmul  22037  evlslem2  22088  evlslem3  22089  evlsgsumadd  22100  mhpmulcl  22137  coe1tmmul2  22261  coe1tmmul  22262  cply1mul  22282  gsummoncoe1  22294  evls1gsumadd  22310  mamudi  22389  mamudir  22390  mamulid  22429  mamurid  22430  mat1dimmul  22464  mat1mhm  22472  dmatmul  22485  scmatscm  22501  1mavmul  22536  mulmarep1gsum1  22561  mdet0pr  22580  m1detdiag  22585  mdetdiag  22587  mdet0  22594  m2detleib  22619  maducoeval2  22628  madugsum  22631  smadiadetlem1a  22651  smadiadetlem3  22656  smadiadet  22658  cpmatmcllem  22706  mat2pmatghm  22718  mat2pmatmul  22719  pmatcollpw3fi1lem1  22774  idpm2idmp  22789  mp2pm2mplem4  22797  pm2mpghm  22804  monmat2matmon  22812  pm2mp  22813  chfacfscmulgsum  22848  chfacfpmmulgsum  22852  cpmadugsumlemF  22864  cayhamlem4  22876  tdeglem4  26081  tdeglem4OLD  26082  tdeglem2  26083  mdegmullem  26100  coe1mul3  26121  plypf1  26234  tayl0  26384  jensen  27012  amgmlem  27013  subrdom  33140  suborng  33196  xrge0slmod  33227  ressply1invg  33445  drgext0gsca  33492  ply1degltdimlem  33521  fedgmullem2  33529  extdg1id  33556  evls1fldgencl  33560  zringnm  33784  rezh  33797  ringexp0nn  41844  aks6d1c6lem1  41880  amgm2d  43900  amgm3d  43901  amgm4d  43902  2zrng0  47655  cznrng  47672  mgpsumz  47775  ply1mulgsumlem2  47804  amgmwlem  48584  amgmw2d  48586