Theorem crngring 18956

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

Assertion

Ref	Expression
crngring	⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)

Proof of Theorem crngring

Step	Hyp	Ref	Expression
1		eqid 2778	. . 3 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
2	1	iscrng 18952	. 2 ⊢ (𝑅 ∈ CRing ↔ (𝑅 ∈ Ring ∧ (mulGrp‘𝑅) ∈ CMnd))
3	2	simplbi 493	1 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)

Syntax hints:   → wi 4   ∈ wcel 2107  ‘cfv 6137  CMndccmn 18590  mulGrpcmgp 18887  Ringcrg 18945  CRingccrg 18946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-rex 3096  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4674  df-br 4889  df-iota 6101  df-fv 6145  df-cring 18948

This theorem is referenced by:  gsummgp0  19006  prdscrngd  19011  crngbinom  19019  dvdsunit  19061  unitmulclb  19063  unitabl  19066  idsrngd  19265  rmodislmod  19334  quscrng  19648  assa2ass  19730  sraassa  19733  rlmassa  19734  asclrhm  19750  assamulgscmlem2  19757  psrcrng  19821  psrassa  19822  mplcrng  19861  mplassa  19862  mplcoe2  19877  mplbas2  19878  mplmon2mul  19908  mplind  19909  evlslem2  19919  evlslem6  19920  evlslem3  19921  evlslem1  19922  evlseu  19923  evlsval2  19927  evlrhm  19932  evlsscasrng  19933  evlsca  19934  evlsvarsrng  19935  evlvar  19936  mpfind  19943  ply1crng  19975  ply1assa  19976  lply1binom  20083  lply1binomsc  20084  evls1rhmlem  20093  evls1gsumadd  20096  evls1gsummul  20097  evl1val  20100  evl1sca  20105  evl1scad  20106  evl1var  20107  evl1vard  20108  evls1var  20109  evls1scasrng  20110  evls1varsrng  20111  evl1subd  20113  evl1expd  20116  pf1const  20117  pf1id  20118  pf1ind  20126  evl1gsumdlem  20127  evl1gsumd  20128  evl1gsumadd  20129  evl1gsummul  20131  evl1varpw  20132  evl1scvarpw  20134  evl1scvarpwval  20135  evl1gsummon  20136  cnring  20175  zringring  20228  zring0  20235  znzrh2  20300  zncyg  20303  zndvds0  20305  znf1o  20306  zzngim  20307  znfld  20315  znchr  20317  znunit  20318  znrrg  20320  cygznlem3  20324  re0g  20366  mamuvs2  20627  matassa  20665  madetsumid  20683  madetsmelbas  20686  madetsmelbas2  20687  mat1dimcrng  20699  dmatcrng  20724  scmatcrng  20743  mdetleib2  20810  mdetf  20817  m1detdiag  20819  mdetdiaglem  20820  mdetdiag  20821  mdet1  20823  mdetrlin  20824  mdetrsca  20825  mdetrsca2  20826  mdetr0  20827  mdet0  20828  mdetrlin2  20829  mdetralt  20830  mdetero  20832  mdetmul  20845  maducoeval2  20862  maduf  20863  madutpos  20864  madugsum  20865  madurid  20866  madulid  20867  marep01ma  20883  smadiadetlem0  20884  smadiadetlem1a  20886  smadiadetlem3lem2  20890  smadiadetlem3  20891  smadiadetlem4  20892  smadiadet  20893  smadiadetglem1  20894  smadiadetglem2  20895  smadiadetg  20896  matinv  20900  matunit  20901  slesolinv  20903  slesolinvbi  20904  slesolex  20905  cramerimplem1  20906  cramerimplem1OLD  20907  cramerimplem2  20908  cramerimplem3  20909  cramerimp  20910  cramer  20915  mat2pmatmul  20954  mat2pmatmhm  20956  mat2pmatrhm  20957  mat2pmatlin  20958  m2cpmmhm  20968  m2cpmrhm  20969  m2pmfzgsumcl  20971  m2cpmrngiso  20981  monmatcollpw  21002  pmatcollpwlem  21003  pmatcollpw  21004  pmatcollpwfi  21005  pmatcollpw3fi1lem2  21010  pmatcollpwscmat  21014  monmat2matmon  21047  pm2mp  21048  chpmatply1  21055  chpmat1d  21059  chpdmat  21064  chpscmat  21065  chpscmatgsumbin  21067  chpscmatgsummon  21068  chp0mat  21069  chpidmat  21070  chmaidscmat  21071  chfacfscmulcl  21080  chfacfscmul0  21081  chfacfscmulgsum  21083  chfacfpmmulcl  21084  chfacfpmmul0  21085  chfacfpmmulgsum  21087  chfacfpmmulgsum2  21088  cayhamlem1  21089  cpmadurid  21090  cpmidgsumm2pm  21092  cpmidpmatlem2  21094  cpmidpmatlem3  21095  cpmadugsumlemB  21097  cpmadugsumlemC  21098  cpmadugsumlemF  21099  cpmadugsumfi  21100  cpmidgsum2  21102  cpmadumatpolylem1  21104  cpmadumatpolylem2  21105  cpmadumatpoly  21106  cayhamlem2  21107  chcoeffeqlem  21108  cayhamlem4  21111  cayleyhamilton0  21112  cayleyhamiltonALT  21114  cayleyhamilton1  21115  recvs  23364  fta1glem1  24373  fta1g  24375  fta1blem  24376  dchrelbas3  25426  dchrelbasd  25427  dchrzrh1  25432  dchrzrhmul  25434  dchrmulcl  25437  dchrn0  25438  dchrfi  25443  dchrghm  25444  dchrabs  25448  dchrinv  25449  dchrptlem1  25452  dchrptlem2  25453  dchrptlem3  25454  dchrsum2  25456  dchrhash  25459  sum2dchr  25462  lgsqrlem1  25534  lgsqrlem2  25535  lgsqrlem3  25536  lgsqrlem4  25537  lgsdchr  25543  lgseisenlem3  25565  lgseisenlem4  25566  dchrisum0flblem1  25666  dchrisum0re  25671  rdivmuldivd  30361  subofld  30386  mdetpmtr1  30495  mdetpmtr12  30497  madjusmdetlem1  30499  madjusmdetlem4  30502  mdetlap  30504  frlmpwfi  38641  isnumbasgrplem3  38648  mendlmod  38736  idomrootle  38746  idomodle  38747  2zrng0  42967  cznabel  42983  cznrng  42984  crhmsubc  43107  fldcat  43111  fldhmsubc  43113  crhmsubcALTV  43125  fldcatALTV  43129  fldhmsubcALTV  43131  mgpsumz  43170  mgpsumn  43171  evl1at0  43208  evl1at1  43209