Theorem crnggrpd 20483

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 20482	. 2 ⊢ (𝜑 → 𝑅 ∈ Ring)
3	2	ringgrpd 20478	1 ⊢ (𝜑 → 𝑅 ∈ Grp)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  Grpcgrp 19153  CRingccrg 20469

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-nul 5259

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rab 3413  df-v 3452  df-sbc 3739  df-ss 3897  df-dif 4046  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6497  df-fv 6551  df-ov 7427  df-ring 20470  df-cring 20471

This theorem is used by:  fermltlchr  21844  selvvvval  22460  selvadd  22461  psdmul  22496  psd1  22497  psdpw  22500  ply1chr  22633  ply1fermltlchr  22639  elrgspnsubrunlem1  33858  elrgspnsubrunlem2  33859  erlbr2d  33875  rlocaddval  33880  rloccring  33882  rloc0g  33883  rlocf1  33885  fracerl  33918  gsumind  33956  dflringlem2  34077  ressply1evls1  34147  evl1deg1  34158  evl1deg2  34159  evl1deg3  34160  ply1dg1rt  34162  vr1nz  34175  mplasclco  34198  psrmonprod  34234  mplmonprod  34236  esplyfvn  34259  irngss  34369  extdgfialglem1  34374  irredminply  34398  algextdeglem4  34402  algextdeglem5  34403  aks6d1c1p3  43269  aks6d1c2lem4  43286  aks6d1c6lem2  43330  aks5lem2  43346  evlsbagval  43723  evlselv  43726  prjcrv0  43778