Theorem ringmnd 18556

Description: A ring is a monoid under addition. (Contributed by Mario Carneiro, 7-Jan-2015.)

Assertion

Ref	Expression
ringmnd	|- ( R e. Ring -> R e. Mnd )

Proof of Theorem ringmnd

Step	Hyp	Ref	Expression
1		ringgrp 18552	. 2 |- ( R e. Ring -> R e. Grp )
2		grpmnd 17429	. 2 |- ( R e. Grp -> R e. Mnd )
3	1, 2	syl 17	1 |- ( R e. Ring -> R e. Mnd )

Syntax hints:   -> wi 4   e. wcel 1990   Mndcmnd 17294   Grpcgrp 17422   Ringcrg 18547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-nul 4789

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653  df-grp 17425  df-ring 18549

This theorem is referenced by:  ringmgm  18557  gsummulc1  18606  gsummulc2  18607  gsummgp0  18608  prdsringd  18612  pwsco1rhm  18738  lmodvsmmulgdi  18898  psrlidm  19403  psrridm  19404  mplsubrglem  19439  mplmonmul  19464  evlslem2  19512  evlslem3  19514  coe1tmmul2  19646  coe1tmmul  19647  cply1mul  19664  gsummoncoe1  19674  evls1gsumadd  19689  cnfldmulg  19778  cnsubmlem  19794  gsumfsum  19813  nn0srg  19816  rge0srg  19817  zring0  19828  re0g  19958  uvcresum  20132  mamudi  20209  mamudir  20210  mamulid  20247  mamurid  20248  mat1dimmul  20282  mat1mhm  20290  dmatmul  20303  scmatscm  20319  1mavmul  20354  mulmarep1gsum1  20379  mdet0pr  20398  m1detdiag  20403  mdetdiag  20405  mdet0  20412  m2detleib  20437  maducoeval2  20446  madugsum  20449  smadiadetlem1a  20469  smadiadetlem3  20474  smadiadet  20476  cpmatmcllem  20523  mat2pmatghm  20535  mat2pmatmul  20536  pmatcollpw3fi1lem1  20591  idpm2idmp  20606  mp2pm2mplem4  20614  pm2mpghm  20621  monmat2matmon  20629  pm2mp  20630  chfacfscmulgsum  20665  chfacfpmmulgsum  20669  cpmadugsumlemF  20681  cayhamlem4  20693  tdeglem4  23820  tdeglem2  23821  mdegmullem  23838  coe1mul3  23859  plypf1  23968  tayl0  24116  jensen  24715  amgmlem  24716  suborng  29815  xrge0slmod  29844  zringnm  30004  rezh  30015  amgm2d  38501  amgm3d  38502  amgm4d  38503  2zrng0  41938  cznrng  41955  mgpsumz  42141  ply1mulgsumlem2  42175  amgmwlem  42548  amgmw2d  42550