Theorem crnggrpd 20163

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

Syntax hints:   → wi 4   ∈ wcel 2109  Grpcgrp 18872  CRingccrg 20150

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-nul 5264

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rab 3409  df-v 3452  df-sbc 3757  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393  df-ring 20151  df-cring 20152

This theorem is referenced by:  fermltlchr  21446  psdmul  22060  psd1  22061  psdpw  22064  ply1chr  22200  ply1fermltlchr  22206  elrgspnsubrunlem1  33205  elrgspnsubrunlem2  33206  erlbr2d  33222  rlocaddval  33226  rloccring  33228  rloc0g  33229  rlocf1  33231  fracerl  33263  ressply1evls1  33541  evl1deg1  33552  evl1deg2  33553  evl1deg3  33554  ply1dg1rt  33555  vr1nz  33566  irngss  33689  irredminply  33713  algextdeglem4  33717  algextdeglem5  33718  aks6d1c1p3  42105  aks6d1c2lem4  42122  aks6d1c6lem2  42166  aks5lem2  42182  evlsbagval  42561  selvvvval  42580  evlselv  42582  selvadd  42583  prjcrv0  42628