Theorem ringmnd 20152

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

Syntax hints:   → wi 4   ∈ wcel 2109  Mndcmnd 18661  Ringcrg 20142

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5261

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-sbc 3754  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390  df-grp 18868  df-ring 20144

This theorem is referenced by:  ringmgm  20153  gsummulc1OLD  20223  gsummulc2OLD  20224  gsummulc1  20225  gsummulc2  20226  gsummgp0  20227  prdsringd  20230  pwsco1rhm  20411  lmodvsmmulgdi  20803  rngqiprngimf1  21210  cnfldmulg  21315  cnsubmlem  21331  gsumfsum  21351  nn0srg  21354  rge0srg  21355  zring0  21368  freshmansdream  21484  re0g  21521  uvcresum  21702  psrlidm  21871  psrridm  21872  mplsubrglem  21913  mplmonmul  21943  evlslem2  21986  evlslem3  21987  evlsgsumadd  21998  mhpmulcl  22036  coe1tmmul2  22162  coe1tmmul  22163  cply1mul  22183  gsummoncoe1  22195  evls1gsumadd  22211  mamudi  22290  mamudir  22291  mamulid  22328  mamurid  22329  mat1dimmul  22363  mat1mhm  22371  dmatmul  22384  scmatscm  22400  1mavmul  22435  mulmarep1gsum1  22460  mdet0pr  22479  m1detdiag  22484  mdetdiag  22486  mdet0  22493  m2detleib  22518  maducoeval2  22527  madugsum  22530  smadiadetlem1a  22550  smadiadetlem3  22555  smadiadet  22557  cpmatmcllem  22605  mat2pmatghm  22617  mat2pmatmul  22618  pmatcollpw3fi1lem1  22673  idpm2idmp  22688  mp2pm2mplem4  22696  pm2mpghm  22703  monmat2matmon  22711  pm2mp  22712  chfacfscmulgsum  22747  chfacfpmmulgsum  22751  cpmadugsumlemF  22763  cayhamlem4  22775  tdeglem4  25965  tdeglem2  25966  mdegmullem  25983  coe1mul3  26004  plypf1  26117  tayl0  26269  jensen  26899  amgmlem  26900  elrgspnlem1  33193  elrgspnlem3  33195  subrdom  33235  suborng  33293  xrge0slmod  33319  ressply1invg  33538  drgext0gsca  33587  ply1degltdimlem  33618  fedgmullem2  33626  extdg1id  33661  evls1fldgencl  33665  zringnm  33948  rezh  33959  ringexp0nn  42122  aks6d1c6lem1  42158  amgm2d  44187  amgm3d  44188  amgm4d  44189  2zrng0  48232  cznrng  48249  mgpsumz  48350  ply1mulgsumlem2  48376  amgmwlem  49791  amgmw2d  49793