Theorem crnggrpd 20165

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

Syntax hints:   → wi 4   ∈ wcel 2111  Grpcgrp 18846  CRingccrg 20152

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 2113  ax-9 2121  ax-ext 2703  ax-nul 5242

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 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rab 3396  df-v 3438  df-sbc 3737  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-iota 6437  df-fv 6489  df-ov 7349  df-ring 20153  df-cring 20154

This theorem is referenced by:  fermltlchr  21466  psdmul  22081  psd1  22082  psdpw  22085  ply1chr  22221  ply1fermltlchr  22227  elrgspnsubrunlem1  33214  elrgspnsubrunlem2  33215  erlbr2d  33231  rlocaddval  33235  rloccring  33237  rloc0g  33238  rlocf1  33240  fracerl  33272  gsumind  33310  ressply1evls1  33528  evl1deg1  33539  evl1deg2  33540  evl1deg3  33541  ply1dg1rt  33543  vr1nz  33554  irngss  33700  extdgfialglem1  33705  irredminply  33729  algextdeglem4  33733  algextdeglem5  33734  aks6d1c1p3  42151  aks6d1c2lem4  42168  aks6d1c6lem2  42212  aks5lem2  42228  evlsbagval  42607  selvvvval  42626  evlselv  42628  selvadd  42629  prjcrv0  42674