Theorem crngringd 20329

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

Syntax hints:   → wi 4   ∈ wcel 2143  Ringcrg 20316  CRingccrg 20317

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-iota 6494  df-fv 6546  df-cring 20319

This theorem is referenced by:  crnggrpd  20330  crng12d  20341  crng32d  20342  pwsgprod  20412  idomringd  20813  qusmulcrng  21405  rhmqusnsg  21406  ssdifidlprm  21467  fermltlchr  21660  frobrhm  21706  psrassa  22103  evlslem1  22214  evlsval3  22221  evlsvvvallem  22223  evlsvvvallem2  22224  evlsvvval  22225  evlsexpval  22260  evlsmaprhm  22263  evlsevl  22264  evlvvval  22265  selvcllem5  22271  selvvvval  22274  selvmul  22276  psdvsca  22308  psdmul  22310  psd1  22311  psdascl  22312  psdpw  22314  ply1fermltlchr  22453  evls1expd  22508  evls1fpws  22510  ressply1evl  22511  evls1maprhm  22517  evl1maprhm  22520  mdetrsca  22741  recvs  25286  isunitc  33542  elrgspnsubrunlem1  33548  elrgspnsubrunlem2  33549  elrgspnsubrun  33550  erlbr2d  33565  erler  33566  erld2  33567  rlocaddval  33570  rlocmulval  33571  rloccring  33572  rloc0g  33573  rloc1r  33574  rlocf1  33575  rlocinvunit  33576  rlocisunit  33577  fracerl  33608  fracf1  33609  fracfld  33610  gsumind  33646  znfermltl  33662  unitpidl1  33713  mxidlprmALT  33762  dflringlem  33765  dflringlem2  33766  dflring4  33769  idlsrgmulrssin  33784  rsprprmprmidl  33793  rsprprmprmidlb  33794  rprmndvdsru  33800  rprmirredlem  33801  rprmdvdspow  33804  rprmdvdsprod  33805  1arithufdlem3  33817  zringfrac  33825  evl1fpws  33835  ressply1evls1  33836  ressasclcl  33842  ply1unit  33846  evl1deg1  33847  evl1deg2  33848  evl1deg3  33849  ply1dg1rt  33851  ply1mulrtss  33853  ply1dg3rt0irred  33855  vr1nz  33864  mplasclco  33887  selvascl  33888  selvply1rhmlem2  33892  selvply1rhmlem4  33894  selvply1rhm  33896  selvply1rhm0  33897  evlvarval  33912  evlextv  33913  psrmonprod  33923  mplmonprod  33925  esplyfvaln  33945  esplyindfv  33947  esplyfvn  33948  vietalem  33950  fldgenfldext  34039  evls1fldgencl  34041  fldextrspunlsp  34045  elirng  34057  0ringirng  34060  irngnzply1lem  34061  extdgfialglem1  34063  extdgfialglem2  34064  ply1annidl  34073  ply1annnr  34074  irredminply  34087  algextdeglem4  34091  rtelextdg2lem  34097  cos9thpiminply  34159  zarclsun  34241  zarmxt1  34251  zarcmplem  34252  zndvdchrrhm  42721  fldhmf1  42838  aks6d1c1p2  42857  aks6d1c1p3  42858  aks6d1c1p4  42859  evl1gprodd  42865  aks6d1c2lem4  42875  aks6d1c5lem0  42883  aks6d1c5lem2  42886  aks6d1c5  42887  aks6d1c6lem2  42919  rhmqusspan  42933  aks5lem2  42935  ply1asclzrhval  42936  aks5lem3a  42937  aks5lem5a  42939  riccrng1  43272  evl0  43300  evlsbagval  43301  evlvvvallem  43302  evlselv  43304  evlsmhpvvval  43310  mhphf  43312  mhphf4  43315