Theorem crngringd 20218

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 20217	. 2 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝑅 ∈ Ring)

Syntax hints:   → wi 4   ∈ wcel 2119  Ringcrg 20205  CRingccrg 20206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-iota 6441  df-fv 6493  df-cring 20208

This theorem is referenced by:  crnggrpd  20219  crng12d  20230  crng32d  20231  pwsgprod  20300  idomringd  20700  qusmulcrng  21277  rhmqusnsg  21278  fermltlchr  21504  frobrhm  21550  psrassa  21947  evlslem1  22058  evlsval3  22065  evlsvvvallem  22067  evlsvvvallem2  22068  evlsvvval  22069  evlsexpval  22104  evlsmaprhm  22107  evlsevl  22108  evlvvval  22109  selvcllem5  22115  selvvvval  22118  selvmul  22120  psdvsca  22152  psdmul  22154  psd1  22155  psdascl  22156  psdpw  22158  ply1fermltlchr  22298  evls1expd  22353  evls1fpws  22355  ressply1evl  22356  evls1maprhm  22362  evl1maprhm  22365  mdetrsca  22586  recvs  25131  elrgspnsubrunlem1  33328  elrgspnsubrunlem2  33329  elrgspnsubrun  33330  erlbr2d  33345  erler  33346  rlocaddval  33349  rlocmulval  33350  rloccring  33351  rloc0g  33352  rloc1r  33353  rlocf1  33354  fracerl  33390  fracf1  33391  fracfld  33392  gsumind  33428  znfermltl  33449  ssdifidlprm  33541  mxidlprmALT  33582  idlsrgmulrssin  33596  rsprprmprmidl  33605  rprmndvdsru  33612  rprmirredlem  33613  rprmdvdspow  33616  rprmdvdsprod  33617  1arithufdlem3  33629  zringfrac  33637  evl1fpws  33647  ressply1evls1  33648  ressasclcl  33654  ply1unit  33658  evl1deg1  33659  evl1deg2  33660  evl1deg3  33661  ply1dg1rt  33663  ply1mulrtss  33665  ply1dg3rt0irred  33667  vr1nz  33676  mplasclco  33700  selvascl  33701  selvply1rhmlem2  33705  selvply1rhmlem4  33707  selvply1rhm  33709  selvply1rhm0  33710  evlvarval  33725  evlextv  33726  psrmonprod  33736  mplmonprod  33738  esplyfvaln  33758  esplyindfv  33760  esplyfvn  33761  vietalem  33763  fldgenfldext  33852  evls1fldgencl  33854  fldextrspunlsp  33858  elirng  33870  0ringirng  33873  irngnzply1lem  33874  extdgfialglem1  33876  extdgfialglem2  33877  ply1annidl  33886  ply1annnr  33887  irredminply  33900  algextdeglem4  33904  rtelextdg2lem  33910  cos9thpiminply  33972  zarclsun  34054  zarmxt1  34064  zarcmplem  34065  zndvdchrrhm  42458  fldhmf1  42575  aks6d1c1p2  42594  aks6d1c1p3  42595  aks6d1c1p4  42596  evl1gprodd  42602  aks6d1c2lem4  42612  aks6d1c5lem0  42620  aks6d1c5lem2  42623  aks6d1c5  42624  aks6d1c6lem2  42656  rhmqusspan  42670  aks5lem2  42672  ply1asclzrhval  42673  aks5lem3a  42674  aks5lem5a  42676  riccrng1  43007  evl0  43035  evlsbagval  43036  evlvvvallem  43037  evlselv  43039  evlsmhpvvval  43045  mhphf  43047  mhphf4  43050