Theorem crngringd 20524

Description: A commutative ring is a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised 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 20523	. 2 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
3	1, 2	syl 18	1 ⊢ (𝜑 → 𝑅 ∈ Ring)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  Ringcrg 20510  CRingccrg 20511

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-iota 6520  df-fv 6574  df-cring 20513

This theorem is used by:  crnggrpd  20525  crng12d  20537  crng32d  20538  crng4  20539  pwsgprod  20610  idomringd  21030  qusmulcrng  21631  rhmqusnsg  21632  ssdifidlprm  21693  fermltlchr  21890  frobrhm  21936  psrassa  22335  evlslem1  22446  evlsval3  22453  evlsvvvallem  22455  evlsvvvallem2  22456  evlsvvval  22457  evlsexpval  22492  evlsmaprhm  22495  evlsevl  22496  evlvvval  22497  selvcllem5  22503  selvvvval  22506  selvmul  22508  psdvsca  22540  psdmul  22542  psd1  22543  psdascl  22544  psdpw  22546  ply1fermltlchr  22685  evls1expd  22740  evls1fpws  22742  ressply1evl  22743  evls1maprhm  22749  evl1maprhm  22752  mdetrsca  22973  recvs  25522  isunitc  33901  elrgspnsubrunlem1  33907  elrgspnsubrunlem2  33908  elrgspnsubrun  33909  erlbr2d  33924  erler  33925  erld2  33926  rlocaddval  33929  rlocmulval  33930  rloccring  33931  rloc0g  33932  rloc1r  33933  rlocf1  33934  rlocinvunit  33935  rlocisunit  33936  fracerl  33972  fracf1  33973  fracfld  33974  gsumind  34010  znfermltl  34026  unitpidl1  34078  mxidlprmALT  34127  dflringlem  34130  dflringlem2  34131  dflring4  34134  idlsrgmulrssin  34149  rsprprmprmidl  34158  rsprprmprmidlb  34159  rprmndvdsru  34165  rprmirredlem  34166  rprmdvdspow  34169  rprmdvdsprod  34170  1arithufdlem3  34182  zringfrac  34189  evl1fpws  34199  ressply1evls1  34200  ressasclcl  34206  ply1unit  34210  evl1deg1  34211  evl1deg2  34212  evl1deg3  34213  ply1dg1rt  34215  ply1mulrtss  34217  ply1dg3rt0irred  34219  vr1nz  34228  evls1degle1  34239  evls1rgspncl  34248  rngunsnply1  34249  rngunsnply1chr2lem2  34251  rngunsnply1chr2lem3  34252  mplasclco  34259  selvascl  34260  selvply1rhmlem2  34264  selvply1rhmlem4  34266  selvply1rhm  34268  selvply1rhm0  34269  evlvarval  34284  evlextv  34285  psrmonprod  34295  mplmonprod  34297  esplyfvaln  34317  esplyindfv  34319  esplyfvn  34320  vietalem  34322  fldgenfldext  34411  evls1fldgencl  34413  fldextrspunlsp  34417  elirng  34429  0ringirng  34432  irngnzply1lem  34433  extdgfialglem1  34435  extdgfialglem2  34436  ply1annidl  34445  ply1annnr  34446  irredminply  34459  algextdeglem4  34463  rtelextdg2lem  34469  cos9thpiminply  34531  zarclsun  34613  zarmxt1  34623  zarcmplem  34624  zndvdchrrhm  43289  fldhmf1  43406  aks6d1c1p2  43425  aks6d1c1p3  43426  aks6d1c1p4  43427  evl1gprodd  43433  aks6d1c2lem4  43443  aks6d1c5lem0  43451  aks6d1c5lem2  43454  aks6d1c5  43455  aks6d1c6lem2  43487  rhmqusspan  43501  aks5lem2  43503  ply1asclzrhval  43504  aks5lem3a  43505  aks5lem5a  43507  riccrng1  43848  evl0  43879  evlsbagval  43880  evlvvvallem  43881  evlselv  43883  evlsmhpvvval  43889  mhphf  43891  mhphf4  43894