Theorem crngringd 20198

Description: A commutative ring is a ring. (Contributed by SN, 16-May-2024.)

Hypothesis

Ref	Expression
crngringd.1	⊢ (𝜑 → 𝑅 ∈ CRing)

Assertion

Ref	Expression
crngringd	⊢ (𝜑 → 𝑅 ∈ Ring)

Proof of Theorem crngringd

Step	Hyp	Ref	Expression
1		crngringd.1	. 2 ⊢ (𝜑 → 𝑅 ∈ CRing)
2		crngring 20197	. 2 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝑅 ∈ Ring)

Syntax hints:   → wi 4   ∈ wcel 2098  Ringcrg 20185  CRingccrg 20186

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-br 5150  df-iota 6501  df-fv 6557  df-cring 20188

This theorem is referenced by:  crnggrpd  20199  crng12d  20210  qusmulcrng  21191  rhmqusnsg  21192  idomringd  21274  fermltlchr  21476  psrassa  21935  evlslem1  22050  psdvsca  22111  psdmul  22113  psd1  22114  psdascl  22115  ply1fermltlchr  22256  evls1expd  22311  evls1fpws  22313  ressply1evl  22314  evls1maprhm  22320  evl1maprhm  22323  mdetrsca  22549  recvs  25117  cringmul32d  33028  frobrhm  33033  erlbr2d  33054  erler  33055  rlocaddval  33058  rlocmulval  33059  rloccring  33060  rloc0g  33061  rloc1r  33062  rlocf1  33063  fracerl  33092  fracf1  33093  fracfld  33094  znfermltl  33177  ssdifidlprm  33270  mxidlprmALT  33311  idlsrgmulrssin  33325  rsprprmprmidl  33334  rprmndvdsru  33341  rprmirredlem  33342  rprmdvdspow  33345  rprmdvdsprod  33346  1arithufdlem2  33360  1arithufdlem3  33361  1arithufdlem4  33362  1arithufd  33363  zringfrac  33369  evl1fpws  33377  ply1unit  33386  evl1deg1  33387  ply1dg1rt  33388  ply1mulrtss  33390  ply1dg3rt0irred  33391  evls1fldgencl  33489  elirng  33495  0ringirng  33498  irngnzply1lem  33499  ply1annidl  33504  ply1annnr  33505  irredminply  33515  algextdeglem4  33519  zarclsun  33602  zarmxt1  33612  zarcmplem  33613  zndvdchrrhm  41573  fldhmf1  41693  aks6d1c1p2  41712  aks6d1c1p3  41713  aks6d1c1p4  41714  evl1gprodd  41720  aks6d1c2lem4  41730  aks6d1c5lem0  41738  aks6d1c5lem2  41741  aks6d1c5  41742  aks6d1c6lem2  41774  rhmqusspan  41788  aks5lem2  41790  riccrng1  41896  pwsgprod  41912  evl0  41925  evlsval3  41927  evlsvvvallem  41929  evlsvvvallem2  41930  evlsvvval  41931  evlsbagval  41934  evlsexpval  41935  evlsmaprhm  41938  evlsevl  41939  evlvvval  41941  evlvvvallem  41942  selvcllem5  41950  selvvvval  41953  evlselv  41955  selvmul  41957  evlsmhpvvval  41963  mhphf  41965  mhphf4  41968