Theorem crngringd 20385

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Ringcrg 20372  CRingccrg 20373

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 2732

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  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 6489  df-fv 6541  df-cring 20375

This theorem is used by:  crnggrpd  20386  crng12d  20398  crng32d  20399  crng4  20400  pwsgprod  20470  idomringd  20889  qusmulcrng  21487  rhmqusnsg  21488  ssdifidlprm  21549  fermltlchr  21742  frobrhm  21788  psrassa  22187  evlslem1  22298  evlsval3  22305  evlsvvvallem  22307  evlsvvvallem2  22308  evlsvvval  22309  evlsexpval  22344  evlsmaprhm  22347  evlsevl  22348  evlvvval  22349  selvcllem5  22355  selvvvval  22358  selvmul  22360  psdvsca  22392  psdmul  22394  psd1  22395  psdascl  22396  psdpw  22398  ply1fermltlchr  22537  evls1expd  22592  evls1fpws  22594  ressply1evl  22595  evls1maprhm  22601  evl1maprhm  22604  mdetrsca  22825  recvs  25374  isunitc  33681  elrgspnsubrunlem1  33687  elrgspnsubrunlem2  33688  elrgspnsubrun  33689  erlbr2d  33704  erler  33705  erld2  33706  rlocaddval  33709  rlocmulval  33710  rloccring  33711  rloc0g  33712  rloc1r  33713  rlocf1  33714  rlocinvunit  33715  rlocisunit  33716  fracerl  33747  fracf1  33748  fracfld  33749  gsumind  33785  znfermltl  33801  unitpidl1  33852  mxidlprmALT  33901  dflringlem  33904  dflringlem2  33905  dflring4  33908  idlsrgmulrssin  33923  rsprprmprmidl  33932  rsprprmprmidlb  33933  rprmndvdsru  33939  rprmirredlem  33940  rprmdvdspow  33943  rprmdvdsprod  33944  1arithufdlem3  33956  zringfrac  33964  evl1fpws  33974  ressply1evls1  33975  ressasclcl  33981  ply1unit  33985  evl1deg1  33986  evl1deg2  33987  evl1deg3  33988  ply1dg1rt  33990  ply1mulrtss  33992  ply1dg3rt0irred  33994  vr1nz  34003  mplasclco  34026  selvascl  34027  selvply1rhmlem2  34031  selvply1rhmlem4  34033  selvply1rhm  34035  selvply1rhm0  34036  evlvarval  34051  evlextv  34052  psrmonprod  34062  mplmonprod  34064  esplyfvaln  34084  esplyindfv  34086  esplyfvn  34087  vietalem  34089  fldgenfldext  34178  evls1fldgencl  34180  fldextrspunlsp  34184  elirng  34196  0ringirng  34199  irngnzply1lem  34200  extdgfialglem1  34202  extdgfialglem2  34203  ply1annidl  34212  ply1annnr  34213  irredminply  34226  algextdeglem4  34230  rtelextdg2lem  34236  cos9thpiminply  34298  zarclsun  34380  zarmxt1  34390  zarcmplem  34391  zndvdchrrhm  42839  fldhmf1  42956  aks6d1c1p2  42975  aks6d1c1p3  42976  aks6d1c1p4  42977  evl1gprodd  42983  aks6d1c2lem4  42993  aks6d1c5lem0  43001  aks6d1c5lem2  43004  aks6d1c5  43005  aks6d1c6lem2  43037  rhmqusspan  43051  aks5lem2  43053  ply1asclzrhval  43054  aks5lem3a  43055  aks5lem5a  43057  riccrng1  43403  evl0  43431  evlsbagval  43432  evlvvvallem  43433  evlselv  43435  evlsmhpvvval  43441  mhphf  43443  mhphf4  43446