Theorem crngringd 20243

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

Syntax hints:   → wi 4   ∈ wcel 2108  Ringcrg 20230  CRingccrg 20231

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-cring 20233

This theorem is referenced by:  crnggrpd  20244  crng12d  20255  crng32d  20256  idomringd  20728  qusmulcrng  21294  rhmqusnsg  21295  fermltlchr  21544  frobrhm  21594  psrassa  21993  evlslem1  22106  psdvsca  22168  psdmul  22170  psd1  22171  psdascl  22172  psdpw  22174  ply1fermltlchr  22316  evls1expd  22371  evls1fpws  22373  ressply1evl  22374  evls1maprhm  22380  evl1maprhm  22383  mdetrsca  22609  recvs  25179  elrgspnsubrunlem1  33251  elrgspnsubrunlem2  33252  elrgspnsubrun  33253  erlbr2d  33268  erler  33269  rlocaddval  33272  rlocmulval  33273  rloccring  33274  rloc0g  33275  rloc1r  33276  rlocf1  33277  fracerl  33308  fracf1  33309  fracfld  33310  znfermltl  33394  ssdifidlprm  33486  mxidlprmALT  33527  idlsrgmulrssin  33541  rsprprmprmidl  33550  rprmndvdsru  33557  rprmirredlem  33558  rprmdvdspow  33561  rprmdvdsprod  33562  1arithufdlem3  33574  zringfrac  33582  evl1fpws  33590  ressasclcl  33596  ply1unit  33600  evl1deg1  33601  evl1deg2  33602  evl1deg3  33603  ply1dg1rt  33604  ply1mulrtss  33606  ply1dg3rt0irred  33607  fldgenfldext  33718  evls1fldgencl  33720  fldextrspunlsp  33724  elirng  33736  0ringirng  33739  irngnzply1lem  33740  ply1annidl  33745  ply1annnr  33746  irredminply  33757  algextdeglem4  33761  rtelextdg2lem  33767  zarclsun  33869  zarmxt1  33879  zarcmplem  33880  zndvdchrrhm  41972  fldhmf1  42091  aks6d1c1p2  42110  aks6d1c1p3  42111  aks6d1c1p4  42112  evl1gprodd  42118  aks6d1c2lem4  42128  aks6d1c5lem0  42136  aks6d1c5lem2  42139  aks6d1c5  42140  aks6d1c6lem2  42172  rhmqusspan  42186  aks5lem2  42188  ply1asclzrhval  42189  aks5lem3a  42190  aks5lem5a  42192  riccrng1  42531  pwsgprod  42554  evl0  42567  evlsval3  42569  evlsvvvallem  42571  evlsvvvallem2  42572  evlsvvval  42573  evlsbagval  42576  evlsexpval  42577  evlsmaprhm  42580  evlsevl  42581  evlvvval  42583  evlvvvallem  42584  selvcllem5  42592  selvvvval  42595  evlselv  42597  selvmul  42599  evlsmhpvvval  42605  mhphf  42607  mhphf4  42610