Theorem crnggrpd 20182

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

Syntax hints:   → wi 4   ∈ wcel 2113  Grpcgrp 18863  CRingccrg 20169

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-nul 5251

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rab 3400  df-v 3442  df-sbc 3741  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361  df-ring 20170  df-cring 20171

This theorem is referenced by:  fermltlchr  21484  psdmul  22109  psd1  22110  psdpw  22113  ply1chr  22250  ply1fermltlchr  22256  elrgspnsubrunlem1  33329  elrgspnsubrunlem2  33330  erlbr2d  33346  rlocaddval  33350  rloccring  33352  rloc0g  33353  rlocf1  33355  fracerl  33388  gsumind  33426  ressply1evls1  33646  evl1deg1  33657  evl1deg2  33658  evl1deg3  33659  ply1dg1rt  33661  vr1nz  33674  esplyfvn  33733  irngss  33844  extdgfialglem1  33849  irredminply  33873  algextdeglem4  33877  algextdeglem5  33878  aks6d1c1p3  42364  aks6d1c2lem4  42381  aks6d1c6lem2  42425  aks5lem2  42441  evlsbagval  42812  selvvvval  42828  evlselv  42830  selvadd  42831  prjcrv0  42876