Theorem ringmnd 20503

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  Mndcmnd 18955  Ringcrg 20492

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-nul 5264

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-iota 6515  df-fv 6569  df-ov 7449  df-grp 19179  df-ring 20494

This theorem is used by:  ringmgm  20504  gsummulc1  20578  gsummulc2  20579  gsummgp0  20580  prdsringd  20583  pwsco1rhm  20774  suborng  21166  lmodvsmmulgdi  21205  rngqiprngimf1  21629  cnfldmulg  21743  cnsubmlem  21754  gsumfsum  21773  nn0srg  21776  rge0srg  21777  zring0  21797  freshmansdream  21913  re0g  21951  uvcresum  22132  psrlidm  22302  psrridm  22303  mplsubrglem  22344  mplmonmul  22378  evlslem2  22421  evlslem3  22422  evlsgsumadd  22438  mhpmulcl  22503  coe1tmmul2  22628  coe1tmmul  22629  cply1mul  22647  gsummoncoe1  22659  evls1gsumadd  22675  mamudi  22751  mamudir  22752  mamulid  22789  mamurid  22790  mat1dimmul  22824  mat1mhm  22832  dmatmul  22845  scmatscm  22861  1mavmul  22896  mulmarep1gsum1  22921  mdet0pr  22940  m1detdiag  22945  mdetdiag  22947  mdet0  22954  m2detleib  22979  maducoeval2  22988  madugsum  22991  smadiadetlem1a  23011  smadiadetlem3  23016  smadiadet  23018  cpmatmcllem  23069  mat2pmatghm  23081  mat2pmatmul  23082  pmatcollpw3fi1lem1  23137  idpm2idmp  23152  mp2pm2mplem4  23160  pm2mpghm  23167  monmat2matmon  23175  pm2mp  23176  chfacfscmulgsum  23211  chfacfpmmulgsum  23215  cpmadugsumlemF  23227  cayhamlem4  23239  tdeglem4  26411  tdeglem2  26412  mdegmullem  26429  coe1mul3  26450  plypf1  26564  tayl0  26722  jensen  27349  amgmlem  27350  elrgspnlem1  33879  elrgspnlem3  33881  subrdom  33922  xrge0slmod  33993  ressply1invg  34184  psrmonmul  34265  esplyfval1  34288  drgext0gsca  34307  ply1degltdimlem  34337  fedgmullem2  34345  extdg1id  34381  evls1fldgencl  34385  zringnm  34673  rezh  34684  ringexp0nn  43387  aks6d1c6lem1  43423  amgm2d  45401  amgm3d  45402  amgm4d  45403  2zrng0  49556  cznrng  49573  mgpsumz  49689  ply1mulgsumlem2  49714  amgmwlem  51299  amgmw2d  51301