Theorem crngringd 20227

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

Syntax hints:   → wi 4   ∈ wcel 2114  Ringcrg 20214  CRingccrg 20215

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-cring 20217

This theorem is referenced by:  crnggrpd  20228  crng12d  20239  crng32d  20240  pwsgprod  20309  idomringd  20705  qusmulcrng  21282  rhmqusnsg  21283  fermltlchr  21509  frobrhm  21555  psrassa  21951  evlslem1  22060  evlsval3  22067  evlsvvvallem  22069  evlsvvvallem2  22070  evlsvvval  22071  psdvsca  22130  psdmul  22132  psd1  22133  psdascl  22134  psdpw  22136  ply1fermltlchr  22277  evls1expd  22332  evls1fpws  22334  ressply1evl  22335  evls1maprhm  22341  evl1maprhm  22344  mdetrsca  22568  recvs  25113  elrgspnsubrunlem1  33308  elrgspnsubrunlem2  33309  elrgspnsubrun  33310  erlbr2d  33325  erler  33326  rlocaddval  33329  rlocmulval  33330  rloccring  33331  rloc0g  33332  rloc1r  33333  rlocf1  33334  fracerl  33367  fracf1  33368  fracfld  33369  gsumind  33405  znfermltl  33426  ssdifidlprm  33518  mxidlprmALT  33559  idlsrgmulrssin  33573  rsprprmprmidl  33582  rprmndvdsru  33589  rprmirredlem  33590  rprmdvdspow  33593  rprmdvdsprod  33594  1arithufdlem3  33606  zringfrac  33614  evl1fpws  33624  ressply1evls1  33625  ressasclcl  33631  ply1unit  33635  evl1deg1  33636  evl1deg2  33637  evl1deg3  33638  ply1dg1rt  33640  ply1mulrtss  33642  ply1dg3rt0irred  33644  vr1nz  33653  evlvarval  33685  evlextv  33686  psrmonprod  33696  mplmonprod  33698  esplyfvaln  33718  esplyindfv  33720  esplyfvn  33721  vietalem  33723  fldgenfldext  33812  evls1fldgencl  33814  fldextrspunlsp  33818  elirng  33830  0ringirng  33833  irngnzply1lem  33834  extdgfialglem1  33836  extdgfialglem2  33837  ply1annidl  33846  ply1annnr  33847  irredminply  33860  algextdeglem4  33864  rtelextdg2lem  33870  cos9thpiminply  33932  zarclsun  34014  zarmxt1  34024  zarcmplem  34025  zndvdchrrhm  42412  fldhmf1  42529  aks6d1c1p2  42548  aks6d1c1p3  42549  aks6d1c1p4  42550  evl1gprodd  42556  aks6d1c2lem4  42566  aks6d1c5lem0  42574  aks6d1c5lem2  42577  aks6d1c5  42578  aks6d1c6lem2  42610  rhmqusspan  42624  aks5lem2  42626  ply1asclzrhval  42627  aks5lem3a  42628  aks5lem5a  42630  riccrng1  42966  evl0  42998  evlsbagval  43002  evlsexpval  43003  evlsmaprhm  43006  evlsevl  43007  evlvvval  43008  evlvvvallem  43009  selvcllem5  43015  selvvvval  43018  evlselv  43020  selvmul  43022  evlsmhpvvval  43028  mhphf  43030  mhphf4  43033