Theorem crnggrpd 20328

Description: A commutative ring is a group. (Contributed by SN, 16-May-2024.)

Hypothesis

Ref	Expression
crngringd.1	⊢ (𝜑 → 𝑅 ∈ CRing)

Assertion

Ref	Expression
crnggrpd	⊢ (𝜑 → 𝑅 ∈ Grp)

Proof of Theorem crnggrpd

Step	Hyp	Ref	Expression
1		crngringd.1	. . 3 ⊢ (𝜑 → 𝑅 ∈ CRing)
2	1	crngringd 20327	. 2 ⊢ (𝜑 → 𝑅 ∈ Ring)
3	2	ringgrpd 20323	1 ⊢ (𝜑 → 𝑅 ∈ Grp)

Syntax hints:   → wi 4   ∈ wcel 2149  Grpcgrp 18999  CRingccrg 20315

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-nul 5271

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-ral 3086  df-rab 3424  df-v 3465  df-sbc 3754  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-iota 6493  df-fv 6545  df-ov 7414  df-ring 20316  df-cring 20317

This theorem is referenced by:  fermltlchr  21647  selvvvval  22261  selvadd  22262  psdmul  22297  psd1  22298  psdpw  22301  ply1chr  22434  ply1fermltlchr  22440  elrgspnsubrunlem1  33507  elrgspnsubrunlem2  33508  erlbr2d  33524  rlocaddval  33529  rloccring  33531  rloc0g  33532  rlocf1  33534  fracerl  33569  gsumind  33607  dflringlem2  33729  ressply1evls1  33799  evl1deg1  33810  evl1deg2  33811  evl1deg3  33812  ply1dg1rt  33814  vr1nz  33827  mplasclco  33850  psrmonprod  33886  mplmonprod  33888  esplyfvn  33911  irngss  34021  extdgfialglem1  34026  irredminply  34050  algextdeglem4  34054  algextdeglem5  34055  aks6d1c1p3  42766  aks6d1c2lem4  42783  aks6d1c6lem2  42827  aks5lem2  42843  evlsbagval  43209  evlselv  43212  prjcrv0  43256