Theorem crngringd 20351

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  Ringcrg 20338  CRingccrg 20339

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 2148  ax-9 2156  ax-ext 2737

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 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-cring 20341

This theorem is used by:  crnggrpd  20352  crng12d  20364  crng32d  20365  crng4  20366  pwsgprod  20436  idomringd  20855  qusmulcrng  21453  rhmqusnsg  21454  ssdifidlprm  21515  fermltlchr  21708  frobrhm  21754  psrassa  22151  evlslem1  22262  evlsval3  22269  evlsvvvallem  22271  evlsvvvallem2  22272  evlsvvval  22273  evlsexpval  22308  evlsmaprhm  22311  evlsevl  22312  evlvvval  22313  selvcllem5  22319  selvvvval  22322  selvmul  22324  psdvsca  22356  psdmul  22358  psd1  22359  psdascl  22360  psdpw  22362  ply1fermltlchr  22501  evls1expd  22556  evls1fpws  22558  ressply1evl  22559  evls1maprhm  22565  evl1maprhm  22568  mdetrsca  22789  recvs  25334  isunitc  33584  elrgspnsubrunlem1  33590  elrgspnsubrunlem2  33591  elrgspnsubrun  33592  erlbr2d  33607  erler  33608  erld2  33609  rlocaddval  33612  rlocmulval  33613  rloccring  33614  rloc0g  33615  rloc1r  33616  rlocf1  33617  rlocinvunit  33618  rlocisunit  33619  fracerl  33650  fracf1  33651  fracfld  33652  gsumind  33688  znfermltl  33704  unitpidl1  33755  mxidlprmALT  33804  dflringlem  33807  dflringlem2  33808  dflring4  33811  idlsrgmulrssin  33826  rsprprmprmidl  33835  rsprprmprmidlb  33836  rprmndvdsru  33842  rprmirredlem  33843  rprmdvdspow  33846  rprmdvdsprod  33847  1arithufdlem3  33859  zringfrac  33867  evl1fpws  33877  ressply1evls1  33878  ressasclcl  33884  ply1unit  33888  evl1deg1  33889  evl1deg2  33890  evl1deg3  33891  ply1dg1rt  33893  ply1mulrtss  33895  ply1dg3rt0irred  33897  vr1nz  33906  mplasclco  33929  selvascl  33930  selvply1rhmlem2  33934  selvply1rhmlem4  33936  selvply1rhm  33938  selvply1rhm0  33939  evlvarval  33954  evlextv  33955  psrmonprod  33965  mplmonprod  33967  esplyfvaln  33987  esplyindfv  33989  esplyfvn  33990  vietalem  33992  fldgenfldext  34081  evls1fldgencl  34083  fldextrspunlsp  34087  elirng  34099  0ringirng  34102  irngnzply1lem  34103  extdgfialglem1  34105  extdgfialglem2  34106  ply1annidl  34115  ply1annnr  34116  irredminply  34129  algextdeglem4  34133  rtelextdg2lem  34139  cos9thpiminply  34201  zarclsun  34283  zarmxt1  34293  zarcmplem  34294  zndvdchrrhm  42773  fldhmf1  42890  aks6d1c1p2  42909  aks6d1c1p3  42910  aks6d1c1p4  42911  evl1gprodd  42917  aks6d1c2lem4  42927  aks6d1c5lem0  42935  aks6d1c5lem2  42938  aks6d1c5  42939  aks6d1c6lem2  42971  rhmqusspan  42985  aks5lem2  42987  ply1asclzrhval  42988  aks5lem3a  42989  aks5lem5a  42991  riccrng1  43322  evl0  43350  evlsbagval  43351  evlvvvallem  43352  evlselv  43354  evlsmhpvvval  43360  mhphf  43362  mhphf4  43365