Theorem crngringd 20324

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

Syntax hints:   → wi 4   ∈ wcel 2149  Ringcrg 20311  CRingccrg 20312

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-iota 6489  df-fv 6541  df-cring 20314

This theorem is referenced by:  crnggrpd  20325  crng12d  20336  crng32d  20337  pwsgprod  20407  idomringd  20808  qusmulcrng  21391  rhmqusnsg  21392  ssdifidlprm  21451  fermltlchr  21644  frobrhm  21690  psrassa  22087  evlslem1  22198  evlsval3  22205  evlsvvvallem  22207  evlsvvvallem2  22208  evlsvvval  22209  evlsexpval  22244  evlsmaprhm  22247  evlsevl  22248  evlvvval  22249  selvcllem5  22255  selvvvval  22258  selvmul  22260  psdvsca  22292  psdmul  22294  psd1  22295  psdascl  22296  psdpw  22298  ply1fermltlchr  22437  evls1expd  22492  evls1fpws  22494  ressply1evl  22495  evls1maprhm  22501  evl1maprhm  22504  mdetrsca  22725  recvs  25270  isunitc  33498  elrgspnsubrunlem1  33504  elrgspnsubrunlem2  33505  elrgspnsubrun  33506  erlbr2d  33521  erler  33522  erld2  33523  rlocaddval  33526  rlocmulval  33527  rloccring  33528  rloc0g  33529  rloc1r  33530  rlocf1  33531  rlocinvunit  33532  rlocisunit  33533  fracerl  33566  fracf1  33567  fracfld  33568  gsumind  33604  znfermltl  33620  unitpidl1  33672  mxidlprmALT  33722  dflringlem  33725  dflringlem2  33726  dflring4  33729  idlsrgmulrssin  33744  rsprprmprmidl  33753  rsprprmprmidlb  33754  rprmndvdsru  33760  rprmirredlem  33761  rprmdvdspow  33764  rprmdvdsprod  33765  1arithufdlem3  33777  zringfrac  33785  evl1fpws  33795  ressply1evls1  33796  ressasclcl  33802  ply1unit  33806  evl1deg1  33807  evl1deg2  33808  evl1deg3  33809  ply1dg1rt  33811  ply1mulrtss  33813  ply1dg3rt0irred  33815  vr1nz  33824  mplasclco  33847  selvascl  33848  selvply1rhmlem2  33852  selvply1rhmlem4  33854  selvply1rhm  33856  selvply1rhm0  33857  evlvarval  33872  evlextv  33873  psrmonprod  33883  mplmonprod  33885  esplyfvaln  33905  esplyindfv  33907  esplyfvn  33908  vietalem  33910  fldgenfldext  33999  evls1fldgencl  34001  fldextrspunlsp  34005  elirng  34017  0ringirng  34020  irngnzply1lem  34021  extdgfialglem1  34023  extdgfialglem2  34024  ply1annidl  34033  ply1annnr  34034  irredminply  34047  algextdeglem4  34051  rtelextdg2lem  34057  cos9thpiminply  34119  zarclsun  34201  zarmxt1  34211  zarcmplem  34212  zndvdchrrhm  42625  fldhmf1  42742  aks6d1c1p2  42761  aks6d1c1p3  42762  aks6d1c1p4  42763  evl1gprodd  42769  aks6d1c2lem4  42779  aks6d1c5lem0  42787  aks6d1c5lem2  42790  aks6d1c5  42791  aks6d1c6lem2  42823  rhmqusspan  42837  aks5lem2  42839  ply1asclzrhval  42840  aks5lem3a  42841  aks5lem5a  42843  riccrng1  43174  evl0  43202  evlsbagval  43203  evlvvvallem  43204  evlselv  43206  evlsmhpvvval  43212  mhphf  43214  mhphf4  43217