Theorem crngringd 20273

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

Syntax hints:   → wi 4   ∈ wcel 2108  Ringcrg 20260  CRingccrg 20261

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-cring 20263

This theorem is referenced by:  crnggrpd  20274  crng12d  20285  idomringd  20750  qusmulcrng  21317  rhmqusnsg  21318  fermltlchr  21567  frobrhm  21617  psrassa  22016  evlslem1  22129  psdvsca  22191  psdmul  22193  psd1  22194  psdascl  22195  ply1fermltlchr  22337  evls1expd  22392  evls1fpws  22394  ressply1evl  22395  evls1maprhm  22401  evl1maprhm  22404  mdetrsca  22630  recvs  25198  cringmul32d  33208  erlbr2d  33236  erler  33237  rlocaddval  33240  rlocmulval  33241  rloccring  33242  rloc0g  33243  rloc1r  33244  rlocf1  33245  fracerl  33273  fracf1  33274  fracfld  33275  znfermltl  33359  ssdifidlprm  33451  mxidlprmALT  33492  idlsrgmulrssin  33506  rsprprmprmidl  33515  rprmndvdsru  33522  rprmirredlem  33523  rprmdvdspow  33526  rprmdvdsprod  33527  1arithufdlem3  33539  zringfrac  33547  evl1fpws  33555  ressasclcl  33561  ply1unit  33565  evl1deg1  33566  evl1deg2  33567  evl1deg3  33568  ply1dg1rt  33569  ply1mulrtss  33571  ply1dg3rt0irred  33572  fldgenfldext  33678  evls1fldgencl  33680  elirng  33686  0ringirng  33689  irngnzply1lem  33690  ply1annidl  33695  ply1annnr  33696  irredminply  33707  algextdeglem4  33711  rtelextdg2lem  33717  zarclsun  33816  zarmxt1  33826  zarcmplem  33827  zndvdchrrhm  41927  fldhmf1  42047  aks6d1c1p2  42066  aks6d1c1p3  42067  aks6d1c1p4  42068  evl1gprodd  42074  aks6d1c2lem4  42084  aks6d1c5lem0  42092  aks6d1c5lem2  42095  aks6d1c5  42096  aks6d1c6lem2  42128  rhmqusspan  42142  aks5lem2  42144  ply1asclzrhval  42145  aks5lem3a  42146  aks5lem5a  42148  riccrng1  42476  pwsgprod  42499  evl0  42512  evlsval3  42514  evlsvvvallem  42516  evlsvvvallem2  42517  evlsvvval  42518  evlsbagval  42521  evlsexpval  42522  evlsmaprhm  42525  evlsevl  42526  evlvvval  42528  evlvvvallem  42529  selvcllem5  42537  selvvvval  42540  evlselv  42542  selvmul  42544  evlsmhpvvval  42550  mhphf  42552  mhphf4  42555