Theorem crnggrpd 20373

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  Grpcgrp 19044  CRingccrg 20360

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-nul 5271

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3082  df-rab 3419  df-v 3459  df-sbc 3747  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7422  df-ring 20361  df-cring 20362

This theorem is used by:  fermltlchr  21729  selvvvval  22343  selvadd  22344  psdmul  22379  psd1  22380  psdpw  22383  ply1chr  22516  ply1fermltlchr  22522  elrgspnsubrunlem1  33631  elrgspnsubrunlem2  33632  erlbr2d  33648  rlocaddval  33653  rloccring  33655  rloc0g  33656  rlocf1  33658  fracerl  33691  gsumind  33729  dflringlem2  33849  ressply1evls1  33919  evl1deg1  33930  evl1deg2  33931  evl1deg3  33932  ply1dg1rt  33934  vr1nz  33947  mplasclco  33970  psrmonprod  34006  mplmonprod  34008  esplyfvn  34031  irngss  34141  extdgfialglem1  34146  irredminply  34170  algextdeglem4  34174  algextdeglem5  34175  aks6d1c1p3  42935  aks6d1c2lem4  42952  aks6d1c6lem2  42996  aks5lem2  43012  evlsbagval  43376  evlselv  43379  prjcrv0  43423