Theorem ringmnd 20178

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

Syntax hints:   → wi 4   ∈ wcel 2113  Mndcmnd 18659  Ringcrg 20168

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-nul 5251

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-sbc 3741  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361  df-grp 18866  df-ring 20170

This theorem is referenced by:  ringmgm  20179  gsummulc1OLD  20249  gsummulc2OLD  20250  gsummulc1  20251  gsummulc2  20252  gsummgp0  20253  prdsringd  20256  pwsco1rhm  20435  suborng  20809  lmodvsmmulgdi  20848  rngqiprngimf1  21255  cnfldmulg  21358  cnsubmlem  21369  gsumfsum  21389  nn0srg  21392  rge0srg  21393  zring0  21413  freshmansdream  21529  re0g  21567  uvcresum  21748  psrlidm  21917  psrridm  21918  mplsubrglem  21959  mplmonmul  21991  evlslem2  22034  evlslem3  22035  evlsgsumadd  22051  mhpmulcl  22092  coe1tmmul2  22218  coe1tmmul  22219  cply1mul  22240  gsummoncoe1  22252  evls1gsumadd  22268  mamudi  22347  mamudir  22348  mamulid  22385  mamurid  22386  mat1dimmul  22420  mat1mhm  22428  dmatmul  22441  scmatscm  22457  1mavmul  22492  mulmarep1gsum1  22517  mdet0pr  22536  m1detdiag  22541  mdetdiag  22543  mdet0  22550  m2detleib  22575  maducoeval2  22584  madugsum  22587  smadiadetlem1a  22607  smadiadetlem3  22612  smadiadet  22614  cpmatmcllem  22662  mat2pmatghm  22674  mat2pmatmul  22675  pmatcollpw3fi1lem1  22730  idpm2idmp  22745  mp2pm2mplem4  22753  pm2mpghm  22760  monmat2matmon  22768  pm2mp  22769  chfacfscmulgsum  22804  chfacfpmmulgsum  22808  cpmadugsumlemF  22820  cayhamlem4  22832  tdeglem4  26021  tdeglem2  26022  mdegmullem  26039  coe1mul3  26060  plypf1  26173  tayl0  26325  jensen  26955  amgmlem  26956  elrgspnlem1  33324  elrgspnlem3  33326  subrdom  33367  xrge0slmod  33429  ressply1invg  33650  drgext0gsca  33748  ply1degltdimlem  33779  fedgmullem2  33787  extdg1id  33823  evls1fldgencl  33827  zringnm  34115  rezh  34126  ringexp0nn  42384  aks6d1c6lem1  42420  amgm2d  44435  amgm3d  44436  amgm4d  44437  2zrng0  48486  cznrng  48503  mgpsumz  48604  ply1mulgsumlem2  48629  amgmwlem  50043  amgmw2d  50045