Theorem crngringd 20263

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

Syntax hints:   → wi 4   ∈ wcel 2105  Ringcrg 20250  CRingccrg 20251

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-cring 20253

This theorem is referenced by:  crnggrpd  20264  crng12d  20275  idomringd  20744  qusmulcrng  21311  rhmqusnsg  21312  fermltlchr  21561  frobrhm  21611  psrassa  22010  evlslem1  22123  psdvsca  22185  psdmul  22187  psd1  22188  psdascl  22189  ply1fermltlchr  22331  evls1expd  22386  evls1fpws  22388  ressply1evl  22389  evls1maprhm  22395  evl1maprhm  22398  mdetrsca  22624  recvs  25192  cringmul32d  33217  erlbr2d  33250  erler  33251  rlocaddval  33254  rlocmulval  33255  rloccring  33256  rloc0g  33257  rloc1r  33258  rlocf1  33259  fracerl  33287  fracf1  33288  fracfld  33289  znfermltl  33373  ssdifidlprm  33465  mxidlprmALT  33506  idlsrgmulrssin  33520  rsprprmprmidl  33529  rprmndvdsru  33536  rprmirredlem  33537  rprmdvdspow  33540  rprmdvdsprod  33541  1arithufdlem3  33553  zringfrac  33561  evl1fpws  33569  ressasclcl  33575  ply1unit  33579  evl1deg1  33580  evl1deg2  33581  evl1deg3  33582  ply1dg1rt  33583  ply1mulrtss  33585  ply1dg3rt0irred  33586  fldgenfldext  33692  evls1fldgencl  33694  elirng  33700  0ringirng  33703  irngnzply1lem  33704  ply1annidl  33709  ply1annnr  33710  irredminply  33721  algextdeglem4  33725  rtelextdg2lem  33731  zarclsun  33830  zarmxt1  33840  zarcmplem  33841  zndvdchrrhm  41952  fldhmf1  42071  aks6d1c1p2  42090  aks6d1c1p3  42091  aks6d1c1p4  42092  evl1gprodd  42098  aks6d1c2lem4  42108  aks6d1c5lem0  42116  aks6d1c5lem2  42119  aks6d1c5  42120  aks6d1c6lem2  42152  rhmqusspan  42166  aks5lem2  42168  ply1asclzrhval  42169  aks5lem3a  42170  aks5lem5a  42172  riccrng1  42507  pwsgprod  42530  evl0  42543  evlsval3  42545  evlsvvvallem  42547  evlsvvvallem2  42548  evlsvvval  42549  evlsbagval  42552  evlsexpval  42553  evlsmaprhm  42556  evlsevl  42557  evlvvval  42559  evlvvvallem  42560  selvcllem5  42568  selvvvval  42571  evlselv  42573  selvmul  42575  evlsmhpvvval  42581  mhphf  42583  mhphf4  42586