Theorem crngringd 20211

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

Syntax hints:   → wi 4   ∈ wcel 2107  Ringcrg 20198  CRingccrg 20199

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3420  df-v 3465  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-br 5124  df-iota 6494  df-fv 6549  df-cring 20201

This theorem is referenced by:  crnggrpd  20212  crng12d  20223  crng32d  20224  idomringd  20696  qusmulcrng  21256  rhmqusnsg  21257  fermltlchr  21502  frobrhm  21548  psrassa  21947  evlslem1  22054  psdvsca  22116  psdmul  22118  psd1  22119  psdascl  22120  psdpw  22122  ply1fermltlchr  22264  evls1expd  22319  evls1fpws  22321  ressply1evl  22322  evls1maprhm  22328  evl1maprhm  22331  mdetrsca  22557  recvs  25115  elrgspnsubrunlem1  33190  elrgspnsubrunlem2  33191  elrgspnsubrun  33192  erlbr2d  33207  erler  33208  rlocaddval  33211  rlocmulval  33212  rloccring  33213  rloc0g  33214  rloc1r  33215  rlocf1  33216  fracerl  33248  fracf1  33249  fracfld  33250  znfermltl  33329  ssdifidlprm  33421  mxidlprmALT  33462  idlsrgmulrssin  33476  rsprprmprmidl  33485  rprmndvdsru  33492  rprmirredlem  33493  rprmdvdspow  33496  rprmdvdsprod  33497  1arithufdlem3  33509  zringfrac  33517  evl1fpws  33525  ressasclcl  33531  ply1unit  33535  evl1deg1  33536  evl1deg2  33537  evl1deg3  33538  ply1dg1rt  33539  ply1mulrtss  33541  ply1dg3rt0irred  33542  fldgenfldext  33655  evls1fldgencl  33657  fldextrspunlsp  33661  elirng  33673  0ringirng  33676  irngnzply1lem  33677  ply1annidl  33682  ply1annnr  33683  irredminply  33696  algextdeglem4  33700  rtelextdg2lem  33706  zarclsun  33828  zarmxt1  33838  zarcmplem  33839  zndvdchrrhm  41931  fldhmf1  42050  aks6d1c1p2  42069  aks6d1c1p3  42070  aks6d1c1p4  42071  evl1gprodd  42077  aks6d1c2lem4  42087  aks6d1c5lem0  42095  aks6d1c5lem2  42098  aks6d1c5  42099  aks6d1c6lem2  42131  rhmqusspan  42145  aks5lem2  42147  ply1asclzrhval  42148  aks5lem3a  42149  aks5lem5a  42151  riccrng1  42494  pwsgprod  42517  evl0  42530  evlsval3  42532  evlsvvvallem  42534  evlsvvvallem2  42535  evlsvvval  42536  evlsbagval  42539  evlsexpval  42540  evlsmaprhm  42543  evlsevl  42544  evlvvval  42546  evlvvvallem  42547  selvcllem5  42555  selvvvval  42558  evlselv  42560  selvmul  42562  evlsmhpvvval  42568  mhphf  42570  mhphf4  42573