Theorem ringmnd 19802

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

Syntax hints:   → wi 4   ∈ wcel 2107  Mndcmnd 18394  Ringcrg 19792

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-nul 5231

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-sbc 3718  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-iota 6395  df-fv 6445  df-ov 7287  df-grp 18589  df-ring 19794

This theorem is referenced by:  ringmgm  19803  gsummulc1  19854  gsummulc2  19855  gsummgp0  19856  prdsringd  19860  pwsco1rhm  19991  lmodvsmmulgdi  20167  cnfldmulg  20639  cnsubmlem  20655  gsumfsum  20674  nn0srg  20677  rge0srg  20678  zring0  20689  re0g  20826  uvcresum  21009  psrlidm  21181  psrridm  21182  mplsubrglem  21219  mplmonmul  21246  evlslem2  21298  evlslem3  21299  evlsgsumadd  21310  mhpmulcl  21348  coe1tmmul2  21456  coe1tmmul  21457  cply1mul  21474  gsummoncoe1  21484  evls1gsumadd  21499  mamudi  21559  mamudir  21560  mamulid  21599  mamurid  21600  mat1dimmul  21634  mat1mhm  21642  dmatmul  21655  scmatscm  21671  1mavmul  21706  mulmarep1gsum1  21731  mdet0pr  21750  m1detdiag  21755  mdetdiag  21757  mdet0  21764  m2detleib  21789  maducoeval2  21798  madugsum  21801  smadiadetlem1a  21821  smadiadetlem3  21826  smadiadet  21828  cpmatmcllem  21876  mat2pmatghm  21888  mat2pmatmul  21889  pmatcollpw3fi1lem1  21944  idpm2idmp  21959  mp2pm2mplem4  21967  pm2mpghm  21974  monmat2matmon  21982  pm2mp  21983  chfacfscmulgsum  22018  chfacfpmmulgsum  22022  cpmadugsumlemF  22034  cayhamlem4  22046  tdeglem4  25233  tdeglem4OLD  25234  tdeglem2  25235  mdegmullem  25252  coe1mul3  25273  plypf1  25382  tayl0  25530  jensen  26147  amgmlem  26148  freshmansdream  31493  suborng  31523  xrge0slmod  31557  drgext0gsca  31688  fedgmullem2  31720  extdg1id  31747  zringnm  31917  rezh  31930  amgm2d  41816  amgm3d  41817  amgm4d  41818  2zrng0  45507  cznrng  45524  mgpsumz  45709  ply1mulgsumlem2  45739  amgmwlem  46517  amgmw2d  46519