Theorem crngringd 20149

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

Syntax hints:   → wi 4   ∈ wcel 2109  Ringcrg 20136  CRingccrg 20137

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 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494  df-cring 20139

This theorem is referenced by:  crnggrpd  20150  crng12d  20161  crng32d  20162  idomringd  20631  qusmulcrng  21209  rhmqusnsg  21210  fermltlchr  21454  frobrhm  21500  psrassa  21898  evlslem1  22005  psdvsca  22067  psdmul  22069  psd1  22070  psdascl  22071  psdpw  22073  ply1fermltlchr  22215  evls1expd  22270  evls1fpws  22272  ressply1evl  22273  evls1maprhm  22279  evl1maprhm  22282  mdetrsca  22506  recvs  25062  elrgspnsubrunlem1  33200  elrgspnsubrunlem2  33201  elrgspnsubrun  33202  erlbr2d  33217  erler  33218  rlocaddval  33221  rlocmulval  33222  rloccring  33223  rloc0g  33224  rloc1r  33225  rlocf1  33226  fracerl  33258  fracf1  33259  fracfld  33260  znfermltl  33316  ssdifidlprm  33408  mxidlprmALT  33449  idlsrgmulrssin  33463  rsprprmprmidl  33472  rprmndvdsru  33479  rprmirredlem  33480  rprmdvdspow  33483  rprmdvdsprod  33484  1arithufdlem3  33496  zringfrac  33504  evl1fpws  33512  ressply1evls1  33513  ressasclcl  33519  ply1unit  33523  evl1deg1  33524  evl1deg2  33525  evl1deg3  33526  ply1dg1rt  33527  ply1mulrtss  33529  ply1dg3rt0irred  33530  vr1nz  33538  fldgenfldext  33642  evls1fldgencl  33644  fldextrspunlsp  33648  elirng  33660  0ringirng  33663  irngnzply1lem  33664  ply1annidl  33671  ply1annnr  33672  irredminply  33685  algextdeglem4  33689  rtelextdg2lem  33695  cos9thpiminply  33757  zarclsun  33839  zarmxt1  33849  zarcmplem  33850  zndvdchrrhm  41948  fldhmf1  42066  aks6d1c1p2  42085  aks6d1c1p3  42086  aks6d1c1p4  42087  evl1gprodd  42093  aks6d1c2lem4  42103  aks6d1c5lem0  42111  aks6d1c5lem2  42114  aks6d1c5  42115  aks6d1c6lem2  42147  rhmqusspan  42161  aks5lem2  42163  ply1asclzrhval  42164  aks5lem3a  42165  aks5lem5a  42167  riccrng1  42497  pwsgprod  42520  evl0  42533  evlsval3  42535  evlsvvvallem  42537  evlsvvvallem2  42538  evlsvvval  42539  evlsbagval  42542  evlsexpval  42543  evlsmaprhm  42546  evlsevl  42547  evlvvval  42549  evlvvvallem  42550  selvcllem5  42558  selvvvval  42561  evlselv  42563  selvmul  42565  evlsmhpvvval  42571  mhphf  42573  mhphf4  42576