Theorem crngringd 20218

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

Syntax hints:   → wi 4   ∈ wcel 2114  Ringcrg 20205  CRingccrg 20206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6448  df-fv 6500  df-cring 20208

This theorem is referenced by:  crnggrpd  20219  crng12d  20230  crng32d  20231  pwsgprod  20300  idomringd  20696  qusmulcrng  21274  rhmqusnsg  21275  fermltlchr  21519  frobrhm  21565  psrassa  21961  evlslem1  22070  evlsval3  22077  evlsvvvallem  22079  evlsvvvallem2  22080  evlsvvval  22081  psdvsca  22140  psdmul  22142  psd1  22143  psdascl  22144  psdpw  22146  ply1fermltlchr  22287  evls1expd  22342  evls1fpws  22344  ressply1evl  22345  evls1maprhm  22351  evl1maprhm  22354  mdetrsca  22578  recvs  25123  elrgspnsubrunlem1  33323  elrgspnsubrunlem2  33324  elrgspnsubrun  33325  erlbr2d  33340  erler  33341  rlocaddval  33344  rlocmulval  33345  rloccring  33346  rloc0g  33347  rloc1r  33348  rlocf1  33349  fracerl  33382  fracf1  33383  fracfld  33384  gsumind  33420  znfermltl  33441  ssdifidlprm  33533  mxidlprmALT  33574  idlsrgmulrssin  33588  rsprprmprmidl  33597  rprmndvdsru  33604  rprmirredlem  33605  rprmdvdspow  33608  rprmdvdsprod  33609  1arithufdlem3  33621  zringfrac  33629  evl1fpws  33639  ressply1evls1  33640  ressasclcl  33646  ply1unit  33650  evl1deg1  33651  evl1deg2  33652  evl1deg3  33653  ply1dg1rt  33655  ply1mulrtss  33657  ply1dg3rt0irred  33659  vr1nz  33668  evlvarval  33700  evlextv  33701  psrmonprod  33711  mplmonprod  33713  esplyfvaln  33733  esplyindfv  33735  esplyfvn  33736  vietalem  33738  fldgenfldext  33828  evls1fldgencl  33830  fldextrspunlsp  33834  elirng  33846  0ringirng  33849  irngnzply1lem  33850  extdgfialglem1  33852  extdgfialglem2  33853  ply1annidl  33862  ply1annnr  33863  irredminply  33876  algextdeglem4  33880  rtelextdg2lem  33886  cos9thpiminply  33948  zarclsun  34030  zarmxt1  34040  zarcmplem  34041  zndvdchrrhm  42426  fldhmf1  42543  aks6d1c1p2  42562  aks6d1c1p3  42563  aks6d1c1p4  42564  evl1gprodd  42570  aks6d1c2lem4  42580  aks6d1c5lem0  42588  aks6d1c5lem2  42591  aks6d1c5  42592  aks6d1c6lem2  42624  rhmqusspan  42638  aks5lem2  42640  ply1asclzrhval  42641  aks5lem3a  42642  aks5lem5a  42644  riccrng1  42980  evl0  43012  evlsbagval  43016  evlsexpval  43017  evlsmaprhm  43020  evlsevl  43021  evlvvval  43022  evlvvvallem  43023  selvcllem5  43029  selvvvval  43032  evlselv  43034  selvmul  43036  evlsmhpvvval  43042  mhphf  43044  mhphf4  43047