Theorem crngringd 20193

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

Syntax hints:   → wi 4   ∈ wcel 2114  Ringcrg 20180  CRingccrg 20181

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-cring 20183

This theorem is referenced by:  crnggrpd  20194  crng12d  20205  crng32d  20206  pwsgprod  20277  idomringd  20673  qusmulcrng  21251  rhmqusnsg  21252  fermltlchr  21496  frobrhm  21542  psrassa  21940  evlslem1  22049  evlsval3  22056  evlsvvvallem  22058  evlsvvvallem2  22059  evlsvvval  22060  psdvsca  22119  psdmul  22121  psd1  22122  psdascl  22123  psdpw  22125  ply1fermltlchr  22268  evls1expd  22323  evls1fpws  22325  ressply1evl  22326  evls1maprhm  22332  evl1maprhm  22335  mdetrsca  22559  recvs  25114  elrgspnsubrunlem1  33340  elrgspnsubrunlem2  33341  elrgspnsubrun  33342  erlbr2d  33357  erler  33358  rlocaddval  33361  rlocmulval  33362  rloccring  33363  rloc0g  33364  rloc1r  33365  rlocf1  33366  fracerl  33399  fracf1  33400  fracfld  33401  gsumind  33437  znfermltl  33458  ssdifidlprm  33550  mxidlprmALT  33591  idlsrgmulrssin  33605  rsprprmprmidl  33614  rprmndvdsru  33621  rprmirredlem  33622  rprmdvdspow  33625  rprmdvdsprod  33626  1arithufdlem3  33638  zringfrac  33646  evl1fpws  33656  ressply1evls1  33657  ressasclcl  33663  ply1unit  33667  evl1deg1  33668  evl1deg2  33669  evl1deg3  33670  ply1dg1rt  33672  ply1mulrtss  33674  ply1dg3rt0irred  33676  vr1nz  33685  evlvarval  33717  evlextv  33718  psrmonprod  33728  mplmonprod  33730  esplyfvaln  33750  esplyindfv  33752  esplyfvn  33753  vietalem  33755  fldgenfldext  33845  evls1fldgencl  33847  fldextrspunlsp  33851  elirng  33863  0ringirng  33866  irngnzply1lem  33867  extdgfialglem1  33869  extdgfialglem2  33870  ply1annidl  33879  ply1annnr  33880  irredminply  33893  algextdeglem4  33897  rtelextdg2lem  33903  cos9thpiminply  33965  zarclsun  34047  zarmxt1  34057  zarcmplem  34058  zndvdchrrhm  42339  fldhmf1  42457  aks6d1c1p2  42476  aks6d1c1p3  42477  aks6d1c1p4  42478  evl1gprodd  42484  aks6d1c2lem4  42494  aks6d1c5lem0  42502  aks6d1c5lem2  42505  aks6d1c5  42506  aks6d1c6lem2  42538  rhmqusspan  42552  aks5lem2  42554  ply1asclzrhval  42555  aks5lem3a  42556  aks5lem5a  42558  riccrng1  42888  evl0  42920  evlsbagval  42924  evlsexpval  42925  evlsmaprhm  42928  evlsevl  42929  evlvvval  42930  evlvvvallem  42931  selvcllem5  42937  selvvvval  42940  evlselv  42942  selvmul  42944  evlsmhpvvval  42950  mhphf  42952  mhphf4  42955