Theorem ringmnd 18917

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

Syntax hints:   → wi 4   ∈ wcel 2164  Mndcmnd 17654  Grpcgrp 17783  Ringcrg 18908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-nul 5015

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ral 3122  df-rex 3123  df-rab 3126  df-v 3416  df-sbc 3663  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4147  df-if 4309  df-sn 4400  df-pr 4402  df-op 4406  df-uni 4661  df-br 4876  df-iota 6090  df-fv 6135  df-ov 6913  df-grp 17786  df-ring 18910

This theorem is referenced by:  ringmgm  18918  gsummulc1  18967  gsummulc2  18968  gsummgp0  18969  prdsringd  18973  pwsco1rhm  19101  lmodvsmmulgdi  19261  psrlidm  19771  psrridm  19772  mplsubrglem  19807  mplmonmul  19832  evlslem2  19879  evlslem3  19881  coe1tmmul2  20013  coe1tmmul  20014  cply1mul  20031  gsummoncoe1  20041  evls1gsumadd  20056  cnfldmulg  20145  cnsubmlem  20161  gsumfsum  20180  nn0srg  20183  rge0srg  20184  zring0  20195  re0g  20326  uvcresum  20506  mamudi  20583  mamudir  20584  mamulid  20621  mamurid  20622  mat1dimmul  20657  mat1mhm  20665  dmatmul  20678  scmatscm  20694  1mavmul  20729  mulmarep1gsum1  20754  mdet0pr  20773  m1detdiag  20778  mdetdiag  20780  mdet0  20787  m2detleib  20812  maducoeval2  20821  madugsum  20824  smadiadetlem1a  20845  smadiadetlem3  20850  smadiadet  20852  cpmatmcllem  20900  mat2pmatghm  20912  mat2pmatmul  20913  pmatcollpw3fi1lem1  20968  idpm2idmp  20983  mp2pm2mplem4  20991  pm2mpghm  20998  monmat2matmon  21006  pm2mp  21007  chfacfscmulgsum  21042  chfacfpmmulgsum  21046  cpmadugsumlemF  21058  cayhamlem4  21070  tdeglem4  24226  tdeglem2  24227  mdegmullem  24244  coe1mul3  24265  plypf1  24374  tayl0  24522  jensen  25135  amgmlem  25136  suborng  30356  xrge0slmod  30385  zringnm  30545  rezh  30556  amgm2d  39336  amgm3d  39337  amgm4d  39338  2zrng0  42799  cznrng  42816  mgpsumz  43002  ply1mulgsumlem2  43036  amgmwlem  43454  amgmw2d  43456