Theorem crngringd 20069

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

Syntax hints:   → wi 4   ∈ wcel 2107  Ringcrg 20056  CRingccrg 20057

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-cring 20059

This theorem is referenced by:  crnggrpd  20070  psrassa  21534  evlslem1  21645  mdetrsca  22105  recvs  24662  idomringd  32375  frobrhm  32382  fermltlchr  32478  znfermltl  32479  qusmul  32515  mxidlprmALT  32613  idlsrgmulrssin  32627  evls1expd  32644  evls1fpws  32646  ressply1evl  32647  ply1fermltlchr  32662  elirng  32750  0ringirng  32753  irngnzply1lem  32754  evls1maprhm  32759  ply1annidl  32763  ply1annnr  32764  algextdeglem1  32772  zarclsun  32850  zarmxt1  32860  zarcmplem  32861  fldhmf1  40955  crng12d  41088  riccrng1  41096  pwsgprod  41114  evl0  41129  evlsval3  41131  evlsvvvallem  41133  evlsvvvallem2  41134  evlsvvval  41135  evlsbagval  41138  evlsexpval  41139  evlsmaprhm  41142  evlsevl  41143  evlvvval  41145  evlvvvallem  41146  selvvvval  41157  evlselv  41159  selvmul  41161  evlsmhpvvval  41167  mhphf  41169  mhphf4  41172