Theorem crnggrpd 20386

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Grpcgrp 19057  CRingccrg 20373

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 2147  ax-9 2155  ax-ext 2732  ax-nul 5263

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 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rab 3413  df-v 3452  df-sbc 3740  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6489  df-fv 6541  df-ov 7416  df-ring 20374  df-cring 20375

This theorem is used by:  fermltlchr  21742  selvvvval  22358  selvadd  22359  psdmul  22394  psd1  22395  psdpw  22398  ply1chr  22531  ply1fermltlchr  22537  elrgspnsubrunlem1  33687  elrgspnsubrunlem2  33688  erlbr2d  33704  rlocaddval  33709  rloccring  33711  rloc0g  33712  rlocf1  33714  fracerl  33747  gsumind  33785  dflringlem2  33905  ressply1evls1  33975  evl1deg1  33986  evl1deg2  33987  evl1deg3  33988  ply1dg1rt  33990  vr1nz  34003  mplasclco  34026  psrmonprod  34062  mplmonprod  34064  esplyfvn  34087  irngss  34197  extdgfialglem1  34202  irredminply  34226  algextdeglem4  34230  algextdeglem5  34231  aks6d1c1p3  42976  aks6d1c2lem4  42993  aks6d1c6lem2  43037  aks5lem2  43053  evlsbagval  43432  evlselv  43435  prjcrv0  43479