Theorem crngringd 20181

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

Syntax hints:   → wi 4   ∈ wcel 2113  Ringcrg 20168  CRingccrg 20169

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-cring 20171

This theorem is referenced by:  crnggrpd  20182  crng12d  20193  crng32d  20194  pwsgprod  20265  idomringd  20661  qusmulcrng  21239  rhmqusnsg  21240  fermltlchr  21484  frobrhm  21530  psrassa  21928  evlslem1  22037  evlsval3  22044  evlsvvvallem  22046  evlsvvvallem2  22047  evlsvvval  22048  psdvsca  22107  psdmul  22109  psd1  22110  psdascl  22111  psdpw  22113  ply1fermltlchr  22256  evls1expd  22311  evls1fpws  22313  ressply1evl  22314  evls1maprhm  22320  evl1maprhm  22323  mdetrsca  22547  recvs  25102  elrgspnsubrunlem1  33329  elrgspnsubrunlem2  33330  elrgspnsubrun  33331  erlbr2d  33346  erler  33347  rlocaddval  33350  rlocmulval  33351  rloccring  33352  rloc0g  33353  rloc1r  33354  rlocf1  33355  fracerl  33388  fracf1  33389  fracfld  33390  gsumind  33426  znfermltl  33447  ssdifidlprm  33539  mxidlprmALT  33580  idlsrgmulrssin  33594  rsprprmprmidl  33603  rprmndvdsru  33610  rprmirredlem  33611  rprmdvdspow  33614  rprmdvdsprod  33615  1arithufdlem3  33627  zringfrac  33635  evl1fpws  33645  ressply1evls1  33646  ressasclcl  33652  ply1unit  33656  evl1deg1  33657  evl1deg2  33658  evl1deg3  33659  ply1dg1rt  33661  ply1mulrtss  33663  ply1dg3rt0irred  33665  vr1nz  33674  evlvarval  33706  evlextv  33707  esplyindfv  33732  esplyfvn  33733  vietalem  33735  fldgenfldext  33825  evls1fldgencl  33827  fldextrspunlsp  33831  elirng  33843  0ringirng  33846  irngnzply1lem  33847  extdgfialglem1  33849  extdgfialglem2  33850  ply1annidl  33859  ply1annnr  33860  irredminply  33873  algextdeglem4  33877  rtelextdg2lem  33883  cos9thpiminply  33945  zarclsun  34027  zarmxt1  34037  zarcmplem  34038  zndvdchrrhm  42226  fldhmf1  42344  aks6d1c1p2  42363  aks6d1c1p3  42364  aks6d1c1p4  42365  evl1gprodd  42371  aks6d1c2lem4  42381  aks6d1c5lem0  42389  aks6d1c5lem2  42392  aks6d1c5  42393  aks6d1c6lem2  42425  rhmqusspan  42439  aks5lem2  42441  ply1asclzrhval  42442  aks5lem3a  42443  aks5lem5a  42445  riccrng1  42776  evl0  42808  evlsbagval  42812  evlsexpval  42813  evlsmaprhm  42816  evlsevl  42817  evlvvval  42818  evlvvvallem  42819  selvcllem5  42825  selvvvval  42828  evlselv  42830  selvmul  42832  evlsmhpvvval  42838  mhphf  42840  mhphf4  42843