Theorem crngringd 20155

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

Syntax hints:   → wi 4   ∈ wcel 2109  Ringcrg 20142  CRingccrg 20143

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-cring 20145

This theorem is referenced by:  crnggrpd  20156  crng12d  20167  crng32d  20168  idomringd  20637  qusmulcrng  21194  rhmqusnsg  21195  fermltlchr  21439  frobrhm  21485  psrassa  21882  evlslem1  21989  psdvsca  22051  psdmul  22053  psd1  22054  psdascl  22055  psdpw  22057  ply1fermltlchr  22199  evls1expd  22254  evls1fpws  22256  ressply1evl  22257  evls1maprhm  22263  evl1maprhm  22266  mdetrsca  22490  recvs  25046  elrgspnsubrunlem1  33198  elrgspnsubrunlem2  33199  elrgspnsubrun  33200  erlbr2d  33215  erler  33216  rlocaddval  33219  rlocmulval  33220  rloccring  33221  rloc0g  33222  rloc1r  33223  rlocf1  33224  fracerl  33256  fracf1  33257  fracfld  33258  znfermltl  33337  ssdifidlprm  33429  mxidlprmALT  33470  idlsrgmulrssin  33484  rsprprmprmidl  33493  rprmndvdsru  33500  rprmirredlem  33501  rprmdvdspow  33504  rprmdvdsprod  33505  1arithufdlem3  33517  zringfrac  33525  evl1fpws  33533  ressply1evls1  33534  ressasclcl  33540  ply1unit  33544  evl1deg1  33545  evl1deg2  33546  evl1deg3  33547  ply1dg1rt  33548  ply1mulrtss  33550  ply1dg3rt0irred  33551  vr1nz  33559  fldgenfldext  33663  evls1fldgencl  33665  fldextrspunlsp  33669  elirng  33681  0ringirng  33684  irngnzply1lem  33685  ply1annidl  33692  ply1annnr  33693  irredminply  33706  algextdeglem4  33710  rtelextdg2lem  33716  cos9thpiminply  33778  zarclsun  33860  zarmxt1  33870  zarcmplem  33871  zndvdchrrhm  41960  fldhmf1  42078  aks6d1c1p2  42097  aks6d1c1p3  42098  aks6d1c1p4  42099  evl1gprodd  42105  aks6d1c2lem4  42115  aks6d1c5lem0  42123  aks6d1c5lem2  42126  aks6d1c5  42127  aks6d1c6lem2  42159  rhmqusspan  42173  aks5lem2  42175  ply1asclzrhval  42176  aks5lem3a  42177  aks5lem5a  42179  riccrng1  42509  pwsgprod  42532  evl0  42545  evlsval3  42547  evlsvvvallem  42549  evlsvvvallem2  42550  evlsvvval  42551  evlsbagval  42554  evlsexpval  42555  evlsmaprhm  42558  evlsevl  42559  evlvvval  42561  evlvvvallem  42562  selvcllem5  42570  selvvvval  42573  evlselv  42575  selvmul  42577  evlsmhpvvval  42583  mhphf  42585  mhphf4  42588