Theorem crngringd 20216

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

Syntax hints:   → wi 4   ∈ wcel 2114  Ringcrg 20203  CRingccrg 20204

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6446  df-fv 6498  df-cring 20206

This theorem is referenced by:  crnggrpd  20217  crng12d  20228  crng32d  20229  pwsgprod  20298  idomringd  20694  qusmulcrng  21272  rhmqusnsg  21273  fermltlchr  21517  frobrhm  21563  psrassa  21960  evlslem1  22069  evlsval3  22076  evlsvvvallem  22078  evlsvvvallem2  22079  evlsvvval  22080  psdvsca  22139  psdmul  22141  psd1  22142  psdascl  22143  psdpw  22145  ply1fermltlchr  22286  evls1expd  22341  evls1fpws  22343  ressply1evl  22344  evls1maprhm  22350  evl1maprhm  22353  mdetrsca  22577  recvs  25122  elrgspnsubrunlem1  33328  elrgspnsubrunlem2  33329  elrgspnsubrun  33330  erlbr2d  33345  erler  33346  rlocaddval  33349  rlocmulval  33350  rloccring  33351  rloc0g  33352  rloc1r  33353  rlocf1  33354  fracerl  33387  fracf1  33388  fracfld  33389  gsumind  33425  znfermltl  33446  ssdifidlprm  33538  mxidlprmALT  33579  idlsrgmulrssin  33593  rsprprmprmidl  33602  rprmndvdsru  33609  rprmirredlem  33610  rprmdvdspow  33613  rprmdvdsprod  33614  1arithufdlem3  33626  zringfrac  33634  evl1fpws  33644  ressply1evls1  33645  ressasclcl  33651  ply1unit  33655  evl1deg1  33656  evl1deg2  33657  evl1deg3  33658  ply1dg1rt  33660  ply1mulrtss  33662  ply1dg3rt0irred  33664  vr1nz  33673  evlvarval  33705  evlextv  33706  psrmonprod  33716  mplmonprod  33718  esplyfvaln  33738  esplyindfv  33740  esplyfvn  33741  vietalem  33743  fldgenfldext  33833  evls1fldgencl  33835  fldextrspunlsp  33839  elirng  33851  0ringirng  33854  irngnzply1lem  33855  extdgfialglem1  33857  extdgfialglem2  33858  ply1annidl  33867  ply1annnr  33868  irredminply  33881  algextdeglem4  33885  rtelextdg2lem  33891  cos9thpiminply  33953  zarclsun  34035  zarmxt1  34045  zarcmplem  34046  zndvdchrrhm  42423  fldhmf1  42540  aks6d1c1p2  42559  aks6d1c1p3  42560  aks6d1c1p4  42561  evl1gprodd  42567  aks6d1c2lem4  42577  aks6d1c5lem0  42585  aks6d1c5lem2  42588  aks6d1c5  42589  aks6d1c6lem2  42621  rhmqusspan  42635  aks5lem2  42637  ply1asclzrhval  42638  aks5lem3a  42639  aks5lem5a  42641  riccrng1  42977  evl0  43009  evlsbagval  43013  evlsexpval  43014  evlsmaprhm  43017  evlsevl  43018  evlvvval  43019  evlvvvallem  43020  selvcllem5  43026  selvvvval  43029  evlselv  43031  selvmul  43033  evlsmhpvvval  43039  mhphf  43041  mhphf4  43044