Theorem ringmnd 19526

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

Syntax hints:   → wi 4   ∈ wcel 2112  Mndcmnd 18127  Ringcrg 19516

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-nul 5184

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3400  df-sbc 3684  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-uni 4806  df-br 5040  df-iota 6316  df-fv 6366  df-ov 7194  df-grp 18322  df-ring 19518

This theorem is referenced by:  ringmgm  19527  gsummulc1  19578  gsummulc2  19579  gsummgp0  19580  prdsringd  19584  pwsco1rhm  19712  lmodvsmmulgdi  19888  cnfldmulg  20349  cnsubmlem  20365  gsumfsum  20384  nn0srg  20387  rge0srg  20388  zring0  20399  re0g  20528  uvcresum  20709  psrlidm  20882  psrridm  20883  mplsubrglem  20920  mplmonmul  20947  evlslem2  20993  evlslem3  20994  evlsgsumadd  21005  mhpmulcl  21043  coe1tmmul2  21151  coe1tmmul  21152  cply1mul  21169  gsummoncoe1  21179  evls1gsumadd  21194  mamudi  21254  mamudir  21255  mamulid  21292  mamurid  21293  mat1dimmul  21327  mat1mhm  21335  dmatmul  21348  scmatscm  21364  1mavmul  21399  mulmarep1gsum1  21424  mdet0pr  21443  m1detdiag  21448  mdetdiag  21450  mdet0  21457  m2detleib  21482  maducoeval2  21491  madugsum  21494  smadiadetlem1a  21514  smadiadetlem3  21519  smadiadet  21521  cpmatmcllem  21569  mat2pmatghm  21581  mat2pmatmul  21582  pmatcollpw3fi1lem1  21637  idpm2idmp  21652  mp2pm2mplem4  21660  pm2mpghm  21667  monmat2matmon  21675  pm2mp  21676  chfacfscmulgsum  21711  chfacfpmmulgsum  21715  cpmadugsumlemF  21727  cayhamlem4  21739  tdeglem4  24911  tdeglem4OLD  24912  tdeglem2  24913  mdegmullem  24930  coe1mul3  24951  plypf1  25060  tayl0  25208  jensen  25825  amgmlem  25826  freshmansdream  31157  suborng  31187  xrge0slmod  31216  drgext0gsca  31347  fedgmullem2  31379  extdg1id  31406  zringnm  31576  rezh  31587  amgm2d  41428  amgm3d  41429  amgm4d  41430  2zrng0  45112  cznrng  45129  mgpsumz  45314  ply1mulgsumlem2  45344  amgmwlem  46120  amgmw2d  46122