Theorem ringmnd 20270

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

Syntax hints:   → wi 4   ∈ wcel 2108  Mndcmnd 18772  Ringcrg 20260

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-nul 5324

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-sbc 3805  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451  df-grp 18976  df-ring 20262

This theorem is referenced by:  ringmgm  20271  gsummulc1OLD  20337  gsummulc2OLD  20338  gsummulc1  20339  gsummulc2  20340  gsummgp0  20341  prdsringd  20344  pwsco1rhm  20528  lmodvsmmulgdi  20917  rngqiprngimf1  21333  cnfldmulg  21439  cnsubmlem  21455  gsumfsum  21475  nn0srg  21478  rge0srg  21479  zring0  21492  freshmansdream  21616  re0g  21653  uvcresum  21836  psrlidm  22005  psrridm  22006  mplsubrglem  22047  mplmonmul  22077  evlslem2  22126  evlslem3  22127  evlsgsumadd  22138  mhpmulcl  22176  coe1tmmul2  22300  coe1tmmul  22301  cply1mul  22321  gsummoncoe1  22333  evls1gsumadd  22349  mamudi  22428  mamudir  22429  mamulid  22468  mamurid  22469  mat1dimmul  22503  mat1mhm  22511  dmatmul  22524  scmatscm  22540  1mavmul  22575  mulmarep1gsum1  22600  mdet0pr  22619  m1detdiag  22624  mdetdiag  22626  mdet0  22633  m2detleib  22658  maducoeval2  22667  madugsum  22670  smadiadetlem1a  22690  smadiadetlem3  22695  smadiadet  22697  cpmatmcllem  22745  mat2pmatghm  22757  mat2pmatmul  22758  pmatcollpw3fi1lem1  22813  idpm2idmp  22828  mp2pm2mplem4  22836  pm2mpghm  22843  monmat2matmon  22851  pm2mp  22852  chfacfscmulgsum  22887  chfacfpmmulgsum  22891  cpmadugsumlemF  22903  cayhamlem4  22915  tdeglem4  26119  tdeglem2  26120  mdegmullem  26137  coe1mul3  26158  plypf1  26271  tayl0  26421  jensen  27050  amgmlem  27051  subrdom  33254  suborng  33310  xrge0slmod  33341  ressply1invg  33559  drgext0gsca  33606  ply1degltdimlem  33635  fedgmullem2  33643  extdg1id  33676  evls1fldgencl  33680  zringnm  33904  rezh  33917  ringexp0nn  42091  aks6d1c6lem1  42127  amgm2d  44160  amgm3d  44161  amgm4d  44162  2zrng0  47967  cznrng  47984  mgpsumz  48087  ply1mulgsumlem2  48116  amgmwlem  48896  amgmw2d  48898