Theorem ringmnd 18379

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

Syntax hints:   → wi 4   ∈ wcel 1977  Mndcmnd 17117  Grpcgrp 17245  Ringcrg 18370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-nul 4717

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552  df-grp 17248  df-ring 18372

This theorem is referenced by:  ringmgm  18380  gsummulc1  18429  gsummulc2  18430  gsummgp0  18431  prdsringd  18435  pwsco1rhm  18561  lmodvsmmulgdi  18721  psrlidm  19224  psrridm  19225  mplsubrglem  19260  mplmonmul  19285  evlslem2  19333  evlslem3  19335  coe1tmmul2  19467  coe1tmmul  19468  cply1mul  19485  gsummoncoe1  19495  evls1gsumadd  19510  cnfldmulg  19597  cnsubmlem  19613  gsumfsum  19632  nn0srg  19635  rge0srg  19636  zring0  19647  re0g  19777  uvcresum  19951  mamudi  20028  mamudir  20029  mamulid  20066  mamurid  20067  mat1dimmul  20101  mat1mhm  20109  dmatmul  20122  scmatscm  20138  1mavmul  20173  mulmarep1gsum1  20198  mdet0pr  20217  m1detdiag  20222  mdetdiag  20224  mdet0  20231  m2detleib  20256  maducoeval2  20265  madugsum  20268  smadiadetlem1a  20288  smadiadetlem3  20293  smadiadet  20295  cpmatmcllem  20342  mat2pmatghm  20354  mat2pmatmul  20355  pmatcollpw3fi1lem1  20410  idpm2idmp  20425  mp2pm2mplem4  20433  pm2mpghm  20440  monmat2matmon  20448  pm2mp  20449  chfacfscmulgsum  20484  chfacfpmmulgsum  20488  cpmadugsumlemF  20500  cayhamlem4  20512  tdeglem4  23624  tdeglem2  23625  mdegmullem  23642  coe1mul3  23663  plypf1  23772  tayl0  23920  jensen  24515  amgmlem  24516  suborng  29146  xrge0slmod  29175  zringnm  29332  rezh  29343  amgm2d  37523  amgm3d  37524  amgm4d  37525  2zrng0  41728  cznrng  41747  mgpsumz  41934  ply1mulgsumlem2  41969  amgmwlem  42357  amgmw2d  42359