Theorem ringmnd 18872

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 18868	. 2 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)
2		grpmnd 17745	. 2 ⊢ (𝑅 ∈ Grp → 𝑅 ∈ Mnd)
3	1, 2	syl 17	1 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd)

Syntax hints:   → wi 4   ∈ wcel 2157  Mndcmnd 17609  Grpcgrp 17738  Ringcrg 18863

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777  ax-nul 4983

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2591  df-eu 2609  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-ral 3094  df-rex 3095  df-rab 3098  df-v 3387  df-sbc 3634  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4116  df-if 4278  df-sn 4369  df-pr 4371  df-op 4375  df-uni 4629  df-br 4844  df-iota 6064  df-fv 6109  df-ov 6881  df-grp 17741  df-ring 18865

This theorem is referenced by:  ringmgm  18873  gsummulc1  18922  gsummulc2  18923  gsummgp0  18924  prdsringd  18928  pwsco1rhm  19056  lmodvsmmulgdi  19216  psrlidm  19726  psrridm  19727  mplsubrglem  19762  mplmonmul  19787  evlslem2  19834  evlslem3  19836  coe1tmmul2  19968  coe1tmmul  19969  cply1mul  19986  gsummoncoe1  19996  evls1gsumadd  20011  cnfldmulg  20100  cnsubmlem  20116  gsumfsum  20135  nn0srg  20138  rge0srg  20139  zring0  20150  re0g  20281  uvcresum  20457  mamudi  20534  mamudir  20535  mamulid  20572  mamurid  20573  mat1dimmul  20608  mat1mhm  20616  dmatmul  20629  scmatscm  20645  1mavmul  20680  mulmarep1gsum1  20705  mdet0pr  20724  m1detdiag  20729  mdetdiag  20731  mdet0  20738  m2detleib  20763  maducoeval2  20772  madugsum  20775  smadiadetlem1a  20796  smadiadetlem3  20801  smadiadet  20803  cpmatmcllem  20851  mat2pmatghm  20863  mat2pmatmul  20864  pmatcollpw3fi1lem1  20919  idpm2idmp  20934  mp2pm2mplem4  20942  pm2mpghm  20949  monmat2matmon  20957  pm2mp  20958  chfacfscmulgsum  20993  chfacfpmmulgsum  20997  cpmadugsumlemF  21009  cayhamlem4  21021  tdeglem4  24161  tdeglem2  24162  mdegmullem  24179  coe1mul3  24200  plypf1  24309  tayl0  24457  jensen  25067  amgmlem  25068  suborng  30331  xrge0slmod  30360  zringnm  30520  rezh  30531  amgm2d  39279  amgm3d  39280  amgm4d  39281  2zrng0  42733  cznrng  42750  mgpsumz  42936  ply1mulgsumlem2  42970  amgmwlem  43346  amgmw2d  43348