Theorem crngringd 20479

Description: A commutative ring is a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised 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 20478	. 2 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
3	1, 2	syl 18	1 ⊢ (𝜑 → 𝑅 ∈ Ring)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  Ringcrg 20465  CRingccrg 20466

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6547  df-cring 20468

This theorem is used by:  crnggrpd  20480  crng12d  20492  crng32d  20493  crng4  20494  pwsgprod  20565  idomringd  20985  qusmulcrng  21586  rhmqusnsg  21587  ssdifidlprm  21648  fermltlchr  21841  frobrhm  21887  psrassa  22286  evlslem1  22397  evlsval3  22404  evlsvvvallem  22406  evlsvvvallem2  22407  evlsvvval  22408  evlsexpval  22443  evlsmaprhm  22446  evlsevl  22447  evlvvval  22448  selvcllem5  22454  selvvvval  22457  selvmul  22459  psdvsca  22491  psdmul  22493  psd1  22494  psdascl  22495  psdpw  22497  ply1fermltlchr  22636  evls1expd  22691  evls1fpws  22693  ressply1evl  22694  evls1maprhm  22700  evl1maprhm  22703  mdetrsca  22924  recvs  25473  isunitc  33849  elrgspnsubrunlem1  33855  elrgspnsubrunlem2  33856  elrgspnsubrun  33857  erlbr2d  33872  erler  33873  erld2  33874  rlocaddval  33877  rlocmulval  33878  rloccring  33879  rloc0g  33880  rloc1r  33881  rlocf1  33882  rlocinvunit  33883  rlocisunit  33884  fracerl  33915  fracf1  33916  fracfld  33917  gsumind  33953  znfermltl  33969  unitpidl1  34021  mxidlprmALT  34070  dflringlem  34073  dflringlem2  34074  dflring4  34077  idlsrgmulrssin  34092  rsprprmprmidl  34101  rsprprmprmidlb  34102  rprmndvdsru  34108  rprmirredlem  34109  rprmdvdspow  34112  rprmdvdsprod  34113  1arithufdlem3  34125  zringfrac  34133  evl1fpws  34143  ressply1evls1  34144  ressasclcl  34150  ply1unit  34154  evl1deg1  34155  evl1deg2  34156  evl1deg3  34157  ply1dg1rt  34159  ply1mulrtss  34161  ply1dg3rt0irred  34163  vr1nz  34172  mplasclco  34195  selvascl  34196  selvply1rhmlem2  34200  selvply1rhmlem4  34202  selvply1rhm  34204  selvply1rhm0  34205  evlvarval  34220  evlextv  34221  psrmonprod  34231  mplmonprod  34233  esplyfvaln  34253  esplyindfv  34255  esplyfvn  34256  vietalem  34258  fldgenfldext  34347  evls1fldgencl  34349  fldextrspunlsp  34353  elirng  34365  0ringirng  34368  irngnzply1lem  34369  extdgfialglem1  34371  extdgfialglem2  34372  ply1annidl  34381  ply1annnr  34382  irredminply  34395  algextdeglem4  34399  rtelextdg2lem  34405  cos9thpiminply  34467  zarclsun  34549  zarmxt1  34559  zarcmplem  34560  zndvdchrrhm  43117  fldhmf1  43234  aks6d1c1p2  43253  aks6d1c1p3  43254  aks6d1c1p4  43255  evl1gprodd  43261  aks6d1c2lem4  43271  aks6d1c5lem0  43279  aks6d1c5lem2  43282  aks6d1c5  43283  aks6d1c6lem2  43315  rhmqusspan  43329  aks5lem2  43331  ply1asclzrhval  43332  aks5lem3a  43333  aks5lem5a  43335  riccrng1  43676  evl0  43707  evlsbagval  43708  evlvvvallem  43709  evlselv  43711  evlsmhpvvval  43717  mhphf  43719  mhphf4  43722