Theorem ringmnd 19308

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

Syntax hints:   → wi 4   ∈ wcel 2114  Mndcmnd 17913  Grpcgrp 18105  Ringcrg 19299

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-nul 5212

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-sbc 3775  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-iota 6316  df-fv 6365  df-ov 7161  df-grp 18108  df-ring 19301

This theorem is referenced by:  ringmgm  19309  gsummulc1  19358  gsummulc2  19359  gsummgp0  19360  prdsringd  19364  pwsco1rhm  19492  lmodvsmmulgdi  19671  psrlidm  20185  psrridm  20186  mplsubrglem  20221  mplmonmul  20247  evlslem2  20294  evlslem3  20295  evlsgsumadd  20306  coe1tmmul2  20446  coe1tmmul  20447  cply1mul  20464  gsummoncoe1  20474  evls1gsumadd  20489  cnfldmulg  20579  cnsubmlem  20595  gsumfsum  20614  nn0srg  20617  rge0srg  20618  zring0  20629  re0g  20758  uvcresum  20939  mamudi  21014  mamudir  21015  mamulid  21052  mamurid  21053  mat1dimmul  21087  mat1mhm  21095  dmatmul  21108  scmatscm  21124  1mavmul  21159  mulmarep1gsum1  21184  mdet0pr  21203  m1detdiag  21208  mdetdiag  21210  mdet0  21217  m2detleib  21242  maducoeval2  21251  madugsum  21254  smadiadetlem1a  21274  smadiadetlem3  21279  smadiadet  21281  cpmatmcllem  21328  mat2pmatghm  21340  mat2pmatmul  21341  pmatcollpw3fi1lem1  21396  idpm2idmp  21411  mp2pm2mplem4  21419  pm2mpghm  21426  monmat2matmon  21434  pm2mp  21435  chfacfscmulgsum  21470  chfacfpmmulgsum  21474  cpmadugsumlemF  21486  cayhamlem4  21498  tdeglem4  24656  tdeglem2  24657  mdegmullem  24674  coe1mul3  24695  plypf1  24804  tayl0  24952  jensen  25568  amgmlem  25569  freshmansdream  30861  suborng  30890  xrge0slmod  30919  drgext0gsca  30996  fedgmullem2  31028  extdg1id  31055  zringnm  31203  rezh  31214  amgm2d  40558  amgm3d  40559  amgm4d  40560  2zrng0  44216  cznrng  44233  mgpsumz  44417  ply1mulgsumlem2  44448  amgmwlem  44910  amgmw2d  44912