Theorem ringmnd 18602

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

Syntax hints:   → wi 4   ∈ wcel 2030  Mndcmnd 17341  Grpcgrp 17469  Ringcrg 18593

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-nul 4822

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-iota 5889  df-fv 5934  df-ov 6693  df-grp 17472  df-ring 18595

This theorem is referenced by:  ringmgm  18603  gsummulc1  18652  gsummulc2  18653  gsummgp0  18654  prdsringd  18658  pwsco1rhm  18786  lmodvsmmulgdi  18946  psrlidm  19451  psrridm  19452  mplsubrglem  19487  mplmonmul  19512  evlslem2  19560  evlslem3  19562  coe1tmmul2  19694  coe1tmmul  19695  cply1mul  19712  gsummoncoe1  19722  evls1gsumadd  19737  cnfldmulg  19826  cnsubmlem  19842  gsumfsum  19861  nn0srg  19864  rge0srg  19865  zring0  19876  re0g  20006  uvcresum  20180  mamudi  20257  mamudir  20258  mamulid  20295  mamurid  20296  mat1dimmul  20330  mat1mhm  20338  dmatmul  20351  scmatscm  20367  1mavmul  20402  mulmarep1gsum1  20427  mdet0pr  20446  m1detdiag  20451  mdetdiag  20453  mdet0  20460  m2detleib  20485  maducoeval2  20494  madugsum  20497  smadiadetlem1a  20517  smadiadetlem3  20522  smadiadet  20524  cpmatmcllem  20571  mat2pmatghm  20583  mat2pmatmul  20584  pmatcollpw3fi1lem1  20639  idpm2idmp  20654  mp2pm2mplem4  20662  pm2mpghm  20669  monmat2matmon  20677  pm2mp  20678  chfacfscmulgsum  20713  chfacfpmmulgsum  20717  cpmadugsumlemF  20729  cayhamlem4  20741  tdeglem4  23865  tdeglem2  23866  mdegmullem  23883  coe1mul3  23904  plypf1  24013  tayl0  24161  jensen  24760  amgmlem  24761  suborng  29943  xrge0slmod  29972  zringnm  30132  rezh  30143  amgm2d  38818  amgm3d  38819  amgm4d  38820  2zrng0  42263  cznrng  42280  mgpsumz  42466  ply1mulgsumlem2  42500  amgmwlem  42876  amgmw2d  42878