Theorem ringmnd 19300

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

Syntax hints:   → wi 4   ∈ wcel 2111  Mndcmnd 17903  Grpcgrp 18095  Ringcrg 19290

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-nul 5174

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-ov 7138  df-grp 18098  df-ring 19292

This theorem is referenced by:  ringmgm  19301  gsummulc1  19352  gsummulc2  19353  gsummgp0  19354  prdsringd  19358  pwsco1rhm  19486  lmodvsmmulgdi  19662  cnfldmulg  20123  cnsubmlem  20139  gsumfsum  20158  nn0srg  20161  rge0srg  20162  zring0  20173  re0g  20301  uvcresum  20482  psrlidm  20641  psrridm  20642  mplsubrglem  20677  mplmonmul  20704  evlslem2  20751  evlslem3  20752  evlsgsumadd  20763  coe1tmmul2  20905  coe1tmmul  20906  cply1mul  20923  gsummoncoe1  20933  evls1gsumadd  20948  mamudi  21008  mamudir  21009  mamulid  21046  mamurid  21047  mat1dimmul  21081  mat1mhm  21089  dmatmul  21102  scmatscm  21118  1mavmul  21153  mulmarep1gsum1  21178  mdet0pr  21197  m1detdiag  21202  mdetdiag  21204  mdet0  21211  m2detleib  21236  maducoeval2  21245  madugsum  21248  smadiadetlem1a  21268  smadiadetlem3  21273  smadiadet  21275  cpmatmcllem  21323  mat2pmatghm  21335  mat2pmatmul  21336  pmatcollpw3fi1lem1  21391  idpm2idmp  21406  mp2pm2mplem4  21414  pm2mpghm  21421  monmat2matmon  21429  pm2mp  21430  chfacfscmulgsum  21465  chfacfpmmulgsum  21469  cpmadugsumlemF  21481  cayhamlem4  21493  tdeglem4  24661  tdeglem2  24662  mdegmullem  24679  coe1mul3  24700  plypf1  24809  tayl0  24957  jensen  25574  amgmlem  25575  freshmansdream  30909  suborng  30939  xrge0slmod  30968  drgext0gsca  31082  fedgmullem2  31114  extdg1id  31141  zringnm  31311  rezh  31322  amgm2d  40904  amgm3d  40905  amgm4d  40906  2zrng0  44562  cznrng  44579  mgpsumz  44764  ply1mulgsumlem2  44795  amgmwlem  45330  amgmw2d  45332