Theorem ringmnd 20260

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

Syntax hints:   → wi 4   ∈ wcel 2105  Mndcmnd 18759  Ringcrg 20250

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-nul 5311

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-sbc 3791  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-ov 7433  df-grp 18966  df-ring 20252

This theorem is referenced by:  ringmgm  20261  gsummulc1OLD  20327  gsummulc2OLD  20328  gsummulc1  20329  gsummulc2  20330  gsummgp0  20331  prdsringd  20334  pwsco1rhm  20518  lmodvsmmulgdi  20911  rngqiprngimf1  21327  cnfldmulg  21433  cnsubmlem  21449  gsumfsum  21469  nn0srg  21472  rge0srg  21473  zring0  21486  freshmansdream  21610  re0g  21647  uvcresum  21830  psrlidm  21999  psrridm  22000  mplsubrglem  22041  mplmonmul  22071  evlslem2  22120  evlslem3  22121  evlsgsumadd  22132  mhpmulcl  22170  coe1tmmul2  22294  coe1tmmul  22295  cply1mul  22315  gsummoncoe1  22327  evls1gsumadd  22343  mamudi  22422  mamudir  22423  mamulid  22462  mamurid  22463  mat1dimmul  22497  mat1mhm  22505  dmatmul  22518  scmatscm  22534  1mavmul  22569  mulmarep1gsum1  22594  mdet0pr  22613  m1detdiag  22618  mdetdiag  22620  mdet0  22627  m2detleib  22652  maducoeval2  22661  madugsum  22664  smadiadetlem1a  22684  smadiadetlem3  22689  smadiadet  22691  cpmatmcllem  22739  mat2pmatghm  22751  mat2pmatmul  22752  pmatcollpw3fi1lem1  22807  idpm2idmp  22822  mp2pm2mplem4  22830  pm2mpghm  22837  monmat2matmon  22845  pm2mp  22846  chfacfscmulgsum  22881  chfacfpmmulgsum  22885  cpmadugsumlemF  22897  cayhamlem4  22909  tdeglem4  26113  tdeglem2  26114  mdegmullem  26131  coe1mul3  26152  plypf1  26265  tayl0  26417  jensen  27046  amgmlem  27047  elrgspnlem1  33231  elrgspnlem3  33233  subrdom  33268  suborng  33324  xrge0slmod  33355  ressply1invg  33573  drgext0gsca  33620  ply1degltdimlem  33649  fedgmullem2  33657  extdg1id  33690  evls1fldgencl  33694  zringnm  33918  rezh  33931  ringexp0nn  42115  aks6d1c6lem1  42151  amgm2d  44187  amgm3d  44188  amgm4d  44189  2zrng0  48087  cznrng  48104  mgpsumz  48206  ply1mulgsumlem2  48232  amgmwlem  49032  amgmw2d  49034