Theorem crngringd 20159

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

Syntax hints:   → wi 4   ∈ wcel 2111  Ringcrg 20146  CRingccrg 20147

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-br 5087  df-iota 6432  df-fv 6484  df-cring 20149

This theorem is referenced by:  crnggrpd  20160  crng12d  20171  crng32d  20172  idomringd  20638  qusmulcrng  21216  rhmqusnsg  21217  fermltlchr  21461  frobrhm  21507  psrassa  21905  evlslem1  22012  psdvsca  22074  psdmul  22076  psd1  22077  psdascl  22078  psdpw  22080  ply1fermltlchr  22222  evls1expd  22277  evls1fpws  22279  ressply1evl  22280  evls1maprhm  22286  evl1maprhm  22289  mdetrsca  22513  recvs  25068  elrgspnsubrunlem1  33206  elrgspnsubrunlem2  33207  elrgspnsubrun  33208  erlbr2d  33223  erler  33224  rlocaddval  33227  rlocmulval  33228  rloccring  33229  rloc0g  33230  rloc1r  33231  rlocf1  33232  fracerl  33264  fracf1  33265  fracfld  33266  gsumind  33302  znfermltl  33323  ssdifidlprm  33415  mxidlprmALT  33456  idlsrgmulrssin  33470  rsprprmprmidl  33479  rprmndvdsru  33486  rprmirredlem  33487  rprmdvdspow  33490  rprmdvdsprod  33491  1arithufdlem3  33503  zringfrac  33511  evl1fpws  33519  ressply1evls1  33520  ressasclcl  33526  ply1unit  33530  evl1deg1  33531  evl1deg2  33532  evl1deg3  33533  ply1dg1rt  33535  ply1mulrtss  33537  ply1dg3rt0irred  33538  vr1nz  33546  fldgenfldext  33673  evls1fldgencl  33675  fldextrspunlsp  33679  elirng  33691  0ringirng  33694  irngnzply1lem  33695  extdgfialglem1  33697  extdgfialglem2  33698  ply1annidl  33707  ply1annnr  33708  irredminply  33721  algextdeglem4  33725  rtelextdg2lem  33731  cos9thpiminply  33793  zarclsun  33875  zarmxt1  33885  zarcmplem  33886  zndvdchrrhm  42005  fldhmf1  42123  aks6d1c1p2  42142  aks6d1c1p3  42143  aks6d1c1p4  42144  evl1gprodd  42150  aks6d1c2lem4  42160  aks6d1c5lem0  42168  aks6d1c5lem2  42171  aks6d1c5  42172  aks6d1c6lem2  42204  rhmqusspan  42218  aks5lem2  42220  ply1asclzrhval  42221  aks5lem3a  42222  aks5lem5a  42224  riccrng1  42554  pwsgprod  42577  evl0  42590  evlsval3  42592  evlsvvvallem  42594  evlsvvvallem2  42595  evlsvvval  42596  evlsbagval  42599  evlsexpval  42600  evlsmaprhm  42603  evlsevl  42604  evlvvval  42606  evlvvvallem  42607  selvcllem5  42615  selvvvval  42618  evlselv  42620  selvmul  42622  evlsmhpvvval  42628  mhphf  42630  mhphf4  42633