Theorem ringcmn 20412

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

Assertion

Ref	Expression
ringcmn	⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd)

Proof of Theorem ringcmn

Step	Hyp	Ref	Expression
1		ringabl 20411	. 2 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Abel)
2		ablcmn 19903	. 2 ⊢ (𝑅 ∈ Abel → 𝑅 ∈ CMnd)
3	1, 2	syl 18	1 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  CMndccmn 19896  Abelcabl 19897  Ringcrg 20361

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742  ax-cnex 11173  ax-resscn 11174  ax-1cn 11175  ax-icn 11176  ax-addcl 11177  ax-addrcl 11178  ax-mulcl 11179  ax-mulrcl 11180  ax-mulcom 11181  ax-addass 11182  ax-mulass 11183  ax-distr 11184  ax-i2m1 11185  ax-1ne0 11186  ax-1rid 11187  ax-rnegex 11188  ax-rrecex 11189  ax-cnre 11190  ax-pre-lttri 11191  ax-pre-lttrn 11192  ax-pre-ltadd 11193  ax-pre-mulgt0 11194

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-rmo 3371  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7376  df-ov 7422  df-oprab 7423  df-mpo 7424  df-om 7869  df-2nd 7993  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-er 8700  df-en 8950  df-dom 8951  df-sdom 8952  df-pnf 11262  df-mnf 11263  df-xr 11264  df-ltxr 11265  df-le 11266  df-sub 11460  df-neg 11461  df-nn 12251  df-2 12320  df-sets 17248  df-slot 17266  df-ndx 17278  df-base 17294  df-plusg 17347  df-0g 17518  df-mgm 18722  df-sgrp 18811  df-mnd 18827  df-grp 19049  df-minusg 19050  df-cmn 19898  df-abl 19899  df-mgp 20263  df-ur 20310  df-ring 20363

This theorem is used by:  ringsrg  20428  gsumfsum  21636  nn0srg  21639  rge0srg  21640  freshmansdream  21776  ofldchr  21778  regsumsupp  21824  ip2di  21843  psrlidm  22163  psrridm  22164  psrdir  22167  psrcom  22169  mplmonmul  22239  mplcoe1  22240  evlslem2  22282  evlslem1  22285  evlsgsumadd  22299  mhpmulcl  22364  psropprmul  22449  coe1mul2  22482  coe1fzgsumdlem  22515  gsumsmonply1  22519  gsummoncoe1  22520  lply1binom  22522  evls1gsumadd  22536  evl1gsumdlem  22568  mamucl  22610  mamudi  22612  mamudir  22613  mat1dimmul  22685  dmatmul  22706  mavmulcl  22756  mdetleib2  22797  mdetf  22804  mdetrlin  22811  mdetralt  22817  m2detleib  22840  madugsum  22852  smadiadetlem3lem2  22876  smadiadet  22879  mat2pmatmul  22940  m2pmfzgsumcl  22957  decpmatmul  22981  pmatcollpw1  22985  pmatcollpwfi  22991  pmatcollpw3fi1lem1  22995  pm2mpcl  23006  mply1topmatcl  23014  mp2pm2mplem2  23016  mp2pm2mplem4  23018  mp2pm2mp  23020  pm2mpghm  23025  pm2mpmhmlem2  23028  pm2mp  23034  chfacfscmulgsum  23069  chfacfpmmulgsum  23073  cpmadugsumlemF  23085  cpmadugsumfi  23086  cayhamlem4  23097  tdeglem1  26268  tdeglem3  26269  tdeglem4  26270  plypf1  26422  taylfvallem  26574  taylf  26577  tayl0  26578  taylpfval  26581  jensenlem1  27204  jensenlem2  27205  jensen  27206  amgm  27208  gsummulgc2  33452  elrspunidl  33802  psrmonprod  34008  esplyfvaln  34030  ply1degltdimlem  34078  fedgmullem1  34085  fedgmullem2  34086  mdetpmtr1  34279  zarcmplem  34337  matunitlindflem1  38326  lfladdcl  39905  aks6d1c1  42943  aks6d1c5lem2  42965  mhphflem  43388  ply1mulgsum  49229  amgmwlem  50709