Theorem crnggrpd 20132

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

Syntax hints:   → wi 4   ∈ wcel 2109  Grpcgrp 18841  CRingccrg 20119

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 2701  ax-nul 5256

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 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rab 3403  df-v 3446  df-sbc 3751  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-ov 7372  df-ring 20120  df-cring 20121

This theorem is referenced by:  fermltlchr  21415  psdmul  22029  psd1  22030  psdpw  22033  ply1chr  22169  ply1fermltlchr  22175  elrgspnsubrunlem1  33171  elrgspnsubrunlem2  33172  erlbr2d  33188  rlocaddval  33192  rloccring  33194  rloc0g  33195  rlocf1  33197  fracerl  33229  ressply1evls1  33507  evl1deg1  33518  evl1deg2  33519  evl1deg3  33520  ply1dg1rt  33521  vr1nz  33532  irngss  33655  irredminply  33679  algextdeglem4  33683  algextdeglem5  33684  aks6d1c1p3  42071  aks6d1c2lem4  42088  aks6d1c6lem2  42132  aks5lem2  42148  evlsbagval  42527  selvvvval  42546  evlselv  42548  selvadd  42549  prjcrv0  42594