Theorem crngringd 20466

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Ringcrg 20452  CRingccrg 20453

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 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6493  df-fv 6545  df-cring 20455

This theorem is used by:  crnggrpd  20467  crng12d  20479  crng32d  20480  crng4  20481  pwsgprod  20552  idomringd  20972  qusmulcrng  21573  rhmqusnsg  21574  ssdifidlprm  21635  fermltlchr  21828  frobrhm  21874  psrassa  22273  evlslem1  22384  evlsval3  22391  evlsvvvallem  22393  evlsvvvallem2  22394  evlsvvval  22395  evlsexpval  22430  evlsmaprhm  22433  evlsevl  22434  evlvvval  22435  selvcllem5  22441  selvvvval  22444  selvmul  22446  psdvsca  22478  psdmul  22480  psd1  22481  psdascl  22482  psdpw  22484  ply1fermltlchr  22623  evls1expd  22678  evls1fpws  22680  ressply1evl  22681  evls1maprhm  22687  evl1maprhm  22690  mdetrsca  22911  recvs  25460  isunitc  33795  elrgspnsubrunlem1  33801  elrgspnsubrunlem2  33802  elrgspnsubrun  33803  erlbr2d  33818  erler  33819  erld2  33820  rlocaddval  33823  rlocmulval  33824  rloccring  33825  rloc0g  33826  rloc1r  33827  rlocf1  33828  rlocinvunit  33829  rlocisunit  33830  fracerl  33861  fracf1  33862  fracfld  33863  gsumind  33899  znfermltl  33915  unitpidl1  33967  mxidlprmALT  34016  dflringlem  34019  dflringlem2  34020  dflring4  34023  idlsrgmulrssin  34038  rsprprmprmidl  34047  rsprprmprmidlb  34048  rprmndvdsru  34054  rprmirredlem  34055  rprmdvdspow  34058  rprmdvdsprod  34059  1arithufdlem3  34071  zringfrac  34079  evl1fpws  34089  ressply1evls1  34090  ressasclcl  34096  ply1unit  34100  evl1deg1  34101  evl1deg2  34102  evl1deg3  34103  ply1dg1rt  34105  ply1mulrtss  34107  ply1dg3rt0irred  34109  vr1nz  34118  mplasclco  34141  selvascl  34142  selvply1rhmlem2  34146  selvply1rhmlem4  34148  selvply1rhm  34150  selvply1rhm0  34151  evlvarval  34166  evlextv  34167  psrmonprod  34177  mplmonprod  34179  esplyfvaln  34199  esplyindfv  34201  esplyfvn  34202  vietalem  34204  fldgenfldext  34293  evls1fldgencl  34295  fldextrspunlsp  34299  elirng  34311  0ringirng  34314  irngnzply1lem  34315  extdgfialglem1  34317  extdgfialglem2  34318  ply1annidl  34327  ply1annnr  34328  irredminply  34341  algextdeglem4  34345  rtelextdg2lem  34351  cos9thpiminply  34413  zarclsun  34495  zarmxt1  34505  zarcmplem  34506  zndvdchrrhm  43003  fldhmf1  43120  aks6d1c1p2  43139  aks6d1c1p3  43140  aks6d1c1p4  43141  evl1gprodd  43147  aks6d1c2lem4  43157  aks6d1c5lem0  43165  aks6d1c5lem2  43168  aks6d1c5  43169  aks6d1c6lem2  43201  rhmqusspan  43215  aks5lem2  43217  ply1asclzrhval  43218  aks5lem3a  43219  aks5lem5a  43221  riccrng1  43562  evl0  43593  evlsbagval  43594  evlvvvallem  43595  evlselv  43597  evlsmhpvvval  43603  mhphf  43605  mhphf4  43608