Theorem crnggrpd 20228

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

Syntax hints:   → wi 4   ∈ wcel 2114  Grpcgrp 18909  CRingccrg 20215

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-nul 5241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rab 3390  df-v 3431  df-sbc 3729  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370  df-ring 20216  df-cring 20217

This theorem is referenced by:  fermltlchr  21509  psdmul  22132  psd1  22133  psdpw  22136  ply1chr  22271  ply1fermltlchr  22277  elrgspnsubrunlem1  33308  elrgspnsubrunlem2  33309  erlbr2d  33325  rlocaddval  33329  rloccring  33331  rloc0g  33332  rlocf1  33334  fracerl  33367  gsumind  33405  ressply1evls1  33625  evl1deg1  33636  evl1deg2  33637  evl1deg3  33638  ply1dg1rt  33640  vr1nz  33653  psrmonprod  33696  mplmonprod  33698  esplyfvn  33721  irngss  33831  extdgfialglem1  33836  irredminply  33860  algextdeglem4  33864  algextdeglem5  33865  aks6d1c1p3  42549  aks6d1c2lem4  42566  aks6d1c6lem2  42610  aks5lem2  42626  evlsbagval  43002  selvvvval  43018  evlselv  43020  selvadd  43021  prjcrv0  43066