Theorem crngringd 20131

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

Syntax hints:   → wi 4   ∈ wcel 2109  Ringcrg 20118  CRingccrg 20119

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-cring 20121

This theorem is referenced by:  crnggrpd  20132  crng12d  20143  crng32d  20144  idomringd  20613  qusmulcrng  21170  rhmqusnsg  21171  fermltlchr  21415  frobrhm  21461  psrassa  21858  evlslem1  21965  psdvsca  22027  psdmul  22029  psd1  22030  psdascl  22031  psdpw  22033  ply1fermltlchr  22175  evls1expd  22230  evls1fpws  22232  ressply1evl  22233  evls1maprhm  22239  evl1maprhm  22242  mdetrsca  22466  recvs  25022  elrgspnsubrunlem1  33171  elrgspnsubrunlem2  33172  elrgspnsubrun  33173  erlbr2d  33188  erler  33189  rlocaddval  33192  rlocmulval  33193  rloccring  33194  rloc0g  33195  rloc1r  33196  rlocf1  33197  fracerl  33229  fracf1  33230  fracfld  33231  znfermltl  33310  ssdifidlprm  33402  mxidlprmALT  33443  idlsrgmulrssin  33457  rsprprmprmidl  33466  rprmndvdsru  33473  rprmirredlem  33474  rprmdvdspow  33477  rprmdvdsprod  33478  1arithufdlem3  33490  zringfrac  33498  evl1fpws  33506  ressply1evls1  33507  ressasclcl  33513  ply1unit  33517  evl1deg1  33518  evl1deg2  33519  evl1deg3  33520  ply1dg1rt  33521  ply1mulrtss  33523  ply1dg3rt0irred  33524  vr1nz  33532  fldgenfldext  33636  evls1fldgencl  33638  fldextrspunlsp  33642  elirng  33654  0ringirng  33657  irngnzply1lem  33658  ply1annidl  33665  ply1annnr  33666  irredminply  33679  algextdeglem4  33683  rtelextdg2lem  33689  cos9thpiminply  33751  zarclsun  33833  zarmxt1  33843  zarcmplem  33844  zndvdchrrhm  41933  fldhmf1  42051  aks6d1c1p2  42070  aks6d1c1p3  42071  aks6d1c1p4  42072  evl1gprodd  42078  aks6d1c2lem4  42088  aks6d1c5lem0  42096  aks6d1c5lem2  42099  aks6d1c5  42100  aks6d1c6lem2  42132  rhmqusspan  42146  aks5lem2  42148  ply1asclzrhval  42149  aks5lem3a  42150  aks5lem5a  42152  riccrng1  42482  pwsgprod  42505  evl0  42518  evlsval3  42520  evlsvvvallem  42522  evlsvvvallem2  42523  evlsvvval  42524  evlsbagval  42527  evlsexpval  42528  evlsmaprhm  42531  evlsevl  42532  evlvvval  42534  evlvvvallem  42535  selvcllem5  42543  selvvvval  42546  evlselv  42548  selvmul  42550  evlsmhpvvval  42556  mhphf  42558  mhphf4  42561