Theorem ringmnd 20450

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Mndcmnd 18903  Ringcrg 20439

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-nul 5260

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6487  df-fv 6539  df-ov 7415  df-grp 19127  df-ring 20441

This theorem is used by:  ringmgm  20451  gsummulc1  20525  gsummulc2  20526  gsummgp0  20527  prdsringd  20530  pwsco1rhm  20721  suborng  21113  lmodvsmmulgdi  21152  rngqiprngimf1  21576  cnfldmulg  21690  cnsubmlem  21701  gsumfsum  21720  nn0srg  21723  rge0srg  21724  zring0  21744  freshmansdream  21860  re0g  21898  uvcresum  22079  psrlidm  22249  psrridm  22250  mplsubrglem  22291  mplmonmul  22325  evlslem2  22368  evlslem3  22369  evlsgsumadd  22385  mhpmulcl  22450  coe1tmmul2  22575  coe1tmmul  22576  cply1mul  22594  gsummoncoe1  22606  evls1gsumadd  22622  mamudi  22698  mamudir  22699  mamulid  22736  mamurid  22737  mat1dimmul  22771  mat1mhm  22779  dmatmul  22792  scmatscm  22808  1mavmul  22843  mulmarep1gsum1  22868  mdet0pr  22887  m1detdiag  22892  mdetdiag  22894  mdet0  22901  m2detleib  22926  maducoeval2  22935  madugsum  22938  smadiadetlem1a  22958  smadiadetlem3  22963  smadiadet  22965  cpmatmcllem  23016  mat2pmatghm  23028  mat2pmatmul  23029  pmatcollpw3fi1lem1  23084  idpm2idmp  23099  mp2pm2mplem4  23107  pm2mpghm  23114  monmat2matmon  23122  pm2mp  23123  chfacfscmulgsum  23158  chfacfpmmulgsum  23162  cpmadugsumlemF  23174  cayhamlem4  23186  tdeglem4  26358  tdeglem2  26359  mdegmullem  26376  coe1mul3  26397  plypf1  26511  tayl0  26671  jensen  27298  amgmlem  27299  elrgspnlem1  33785  elrgspnlem3  33787  subrdom  33828  xrge0slmod  33891  ressply1invg  34083  psrmonmul  34164  esplyfval1  34187  drgext0gsca  34206  ply1degltdimlem  34236  fedgmullem2  34244  extdg1id  34280  evls1fldgencl  34284  zringnm  34572  rezh  34583  ringexp0nn  43152  aks6d1c6lem1  43188  amgm2d  45157  amgm3d  45158  amgm4d  45159  2zrng0  49285  cznrng  49302  mgpsumz  49418  ply1mulgsumlem2  49443  amgmwlem  50931  amgmw2d  50933