Theorem ringmnd 20356

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  Mndcmnd 18821  Ringcrg 20346

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-nul 5274

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ne 2962  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-sbc 3748  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-iota 6499  df-fv 6551  df-ov 7426  df-grp 19034  df-ring 20348

This theorem is used by:  ringmgm  20357  gsummulc1  20430  gsummulc2  20431  gsummgp0  20432  prdsringd  20435  pwsco1rhm  20626  suborng  21016  lmodvsmmulgdi  21055  rngqiprngimf1  21477  cnfldmulg  21591  cnsubmlem  21602  gsumfsum  21621  nn0srg  21624  rge0srg  21625  zring0  21645  freshmansdream  21761  re0g  21799  uvcresum  21980  psrlidm  22148  psrridm  22149  mplsubrglem  22190  mplmonmul  22224  evlslem2  22267  evlslem3  22268  evlsgsumadd  22284  mhpmulcl  22349  coe1tmmul2  22474  coe1tmmul  22475  cply1mul  22493  gsummoncoe1  22505  evls1gsumadd  22521  mamudi  22597  mamudir  22598  mamulid  22635  mamurid  22636  mat1dimmul  22670  mat1mhm  22678  dmatmul  22691  scmatscm  22707  1mavmul  22742  mulmarep1gsum1  22767  mdet0pr  22786  m1detdiag  22791  mdetdiag  22793  mdet0  22800  m2detleib  22825  maducoeval2  22834  madugsum  22837  smadiadetlem1a  22857  smadiadetlem3  22862  smadiadet  22864  cpmatmcllem  22912  mat2pmatghm  22924  mat2pmatmul  22925  pmatcollpw3fi1lem1  22980  idpm2idmp  22995  mp2pm2mplem4  23003  pm2mpghm  23010  monmat2matmon  23018  pm2mp  23019  chfacfscmulgsum  23054  chfacfpmmulgsum  23058  cpmadugsumlemF  23070  cayhamlem4  23082  tdeglem4  26254  tdeglem2  26255  mdegmullem  26272  coe1mul3  26293  plypf1  26406  tayl0  26562  jensen  27190  amgmlem  27191  elrgspnlem1  33593  elrgspnlem3  33595  subrdom  33636  xrge0slmod  33699  ressply1invg  33890  psrmonmul  33971  esplyfval1  33994  drgext0gsca  34013  ply1degltdimlem  34043  fedgmullem2  34051  extdg1id  34087  evls1fldgencl  34091  zringnm  34379  rezh  34390  ringexp0nn  42942  aks6d1c6lem1  42978  amgm2d  44965  amgm3d  44966  amgm4d  44967  2zrng0  49050  cznrng  49067  mgpsumz  49183  ply1mulgsumlem2  49208  amgmwlem  50691  amgmw2d  50693