Theorem crnggrpd 20293

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

Syntax hints:   → wi 4   ∈ wcel 2142  Grpcgrp 18975  CRingccrg 20280

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-nul 5256

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3077  df-rab 3415  df-v 3456  df-sbc 3745  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6477  df-fv 6529  df-ov 7399  df-ring 20281  df-cring 20282

This theorem is referenced by:  fermltlchr  21578  selvvvval  22192  selvadd  22193  psdmul  22228  psd1  22229  psdpw  22232  ply1chr  22366  ply1fermltlchr  22372  elrgspnsubrunlem1  33425  elrgspnsubrunlem2  33426  erlbr2d  33442  rlocaddval  33447  rloccring  33449  rloc0g  33450  rlocf1  33452  fracerl  33490  gsumind  33528  dflringlem2  33688  ressply1evls1  33758  evl1deg1  33769  evl1deg2  33770  evl1deg3  33771  ply1dg1rt  33773  vr1nz  33786  mplasclco  33810  psrmonprod  33846  mplmonprod  33848  esplyfvn  33871  irngss  33981  extdgfialglem1  33986  irredminply  34010  algextdeglem4  34014  algextdeglem5  34015  aks6d1c1p3  42724  aks6d1c2lem4  42741  aks6d1c6lem2  42785  aks5lem2  42801  evlsbagval  43165  evlselv  43168  prjcrv0  43212