Theorem crngringd 20162

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

Syntax hints:   → wi 4   ∈ wcel 2109  Ringcrg 20149  CRingccrg 20150

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-cring 20152

This theorem is referenced by:  crnggrpd  20163  crng12d  20174  crng32d  20175  idomringd  20644  qusmulcrng  21201  rhmqusnsg  21202  fermltlchr  21446  frobrhm  21492  psrassa  21889  evlslem1  21996  psdvsca  22058  psdmul  22060  psd1  22061  psdascl  22062  psdpw  22064  ply1fermltlchr  22206  evls1expd  22261  evls1fpws  22263  ressply1evl  22264  evls1maprhm  22270  evl1maprhm  22273  mdetrsca  22497  recvs  25053  elrgspnsubrunlem1  33205  elrgspnsubrunlem2  33206  elrgspnsubrun  33207  erlbr2d  33222  erler  33223  rlocaddval  33226  rlocmulval  33227  rloccring  33228  rloc0g  33229  rloc1r  33230  rlocf1  33231  fracerl  33263  fracf1  33264  fracfld  33265  znfermltl  33344  ssdifidlprm  33436  mxidlprmALT  33477  idlsrgmulrssin  33491  rsprprmprmidl  33500  rprmndvdsru  33507  rprmirredlem  33508  rprmdvdspow  33511  rprmdvdsprod  33512  1arithufdlem3  33524  zringfrac  33532  evl1fpws  33540  ressply1evls1  33541  ressasclcl  33547  ply1unit  33551  evl1deg1  33552  evl1deg2  33553  evl1deg3  33554  ply1dg1rt  33555  ply1mulrtss  33557  ply1dg3rt0irred  33558  vr1nz  33566  fldgenfldext  33670  evls1fldgencl  33672  fldextrspunlsp  33676  elirng  33688  0ringirng  33691  irngnzply1lem  33692  ply1annidl  33699  ply1annnr  33700  irredminply  33713  algextdeglem4  33717  rtelextdg2lem  33723  cos9thpiminply  33785  zarclsun  33867  zarmxt1  33877  zarcmplem  33878  zndvdchrrhm  41967  fldhmf1  42085  aks6d1c1p2  42104  aks6d1c1p3  42105  aks6d1c1p4  42106  evl1gprodd  42112  aks6d1c2lem4  42122  aks6d1c5lem0  42130  aks6d1c5lem2  42133  aks6d1c5  42134  aks6d1c6lem2  42166  rhmqusspan  42180  aks5lem2  42182  ply1asclzrhval  42183  aks5lem3a  42184  aks5lem5a  42186  riccrng1  42516  pwsgprod  42539  evl0  42552  evlsval3  42554  evlsvvvallem  42556  evlsvvvallem2  42557  evlsvvval  42558  evlsbagval  42561  evlsexpval  42562  evlsmaprhm  42565  evlsevl  42566  evlvvval  42568  evlvvvallem  42569  selvcllem5  42577  selvvvval  42580  evlselv  42582  selvmul  42584  evlsmhpvvval  42590  mhphf  42592  mhphf4  42595