Theorem crngringd 20172

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

Syntax hints:   → wi 4   ∈ wcel 2113  Ringcrg 20159  CRingccrg 20160

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 2705

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 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-iota 6445  df-fv 6497  df-cring 20162

This theorem is referenced by:  crnggrpd  20173  crng12d  20184  crng32d  20185  pwsgprod  20256  idomringd  20652  qusmulcrng  21230  rhmqusnsg  21231  fermltlchr  21475  frobrhm  21521  psrassa  21919  evlslem1  22028  evlsval3  22035  evlsvvvallem  22037  evlsvvvallem2  22038  evlsvvval  22039  psdvsca  22098  psdmul  22100  psd1  22101  psdascl  22102  psdpw  22104  ply1fermltlchr  22247  evls1expd  22302  evls1fpws  22304  ressply1evl  22305  evls1maprhm  22311  evl1maprhm  22314  mdetrsca  22538  recvs  25093  elrgspnsubrunlem1  33257  elrgspnsubrunlem2  33258  elrgspnsubrun  33259  erlbr2d  33274  erler  33275  rlocaddval  33278  rlocmulval  33279  rloccring  33280  rloc0g  33281  rloc1r  33282  rlocf1  33283  fracerl  33316  fracf1  33317  fracfld  33318  gsumind  33354  znfermltl  33375  ssdifidlprm  33467  mxidlprmALT  33508  idlsrgmulrssin  33522  rsprprmprmidl  33531  rprmndvdsru  33538  rprmirredlem  33539  rprmdvdspow  33542  rprmdvdsprod  33543  1arithufdlem3  33555  zringfrac  33563  evl1fpws  33573  ressply1evls1  33574  ressasclcl  33580  ply1unit  33584  evl1deg1  33585  evl1deg2  33586  evl1deg3  33587  ply1dg1rt  33589  ply1mulrtss  33591  ply1dg3rt0irred  33593  vr1nz  33602  evlvarval  33634  evlextv  33635  esplyindfv  33660  esplyfvn  33661  vietalem  33663  fldgenfldext  33753  evls1fldgencl  33755  fldextrspunlsp  33759  elirng  33771  0ringirng  33774  irngnzply1lem  33775  extdgfialglem1  33777  extdgfialglem2  33778  ply1annidl  33787  ply1annnr  33788  irredminply  33801  algextdeglem4  33805  rtelextdg2lem  33811  cos9thpiminply  33873  zarclsun  33955  zarmxt1  33965  zarcmplem  33966  zndvdchrrhm  42138  fldhmf1  42256  aks6d1c1p2  42275  aks6d1c1p3  42276  aks6d1c1p4  42277  evl1gprodd  42283  aks6d1c2lem4  42293  aks6d1c5lem0  42301  aks6d1c5lem2  42304  aks6d1c5  42305  aks6d1c6lem2  42337  rhmqusspan  42351  aks5lem2  42353  ply1asclzrhval  42354  aks5lem3a  42355  aks5lem5a  42357  riccrng1  42691  evl0  42723  evlsbagval  42727  evlsexpval  42728  evlsmaprhm  42731  evlsevl  42732  evlvvval  42733  evlvvvallem  42734  selvcllem5  42740  selvvvval  42743  evlselv  42745  selvmul  42747  evlsmhpvvval  42753  mhphf  42755  mhphf4  42758