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 18812  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 5245

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 3395  df-v 3438  df-sbc 3743  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490  df-ov 7352  df-ring 20120  df-cring 20121

This theorem is referenced by:  fermltlchr  21436  psdmul  22051  psd1  22052  psdpw  22055  ply1chr  22191  ply1fermltlchr  22197  elrgspnsubrunlem1  33187  elrgspnsubrunlem2  33188  erlbr2d  33204  rlocaddval  33208  rloccring  33210  rloc0g  33211  rlocf1  33213  fracerl  33245  ressply1evls1  33500  evl1deg1  33511  evl1deg2  33512  evl1deg3  33513  ply1dg1rt  33515  vr1nz  33526  irngss  33654  extdgfialglem1  33659  irredminply  33683  algextdeglem4  33687  algextdeglem5  33688  aks6d1c1p3  42083  aks6d1c2lem4  42100  aks6d1c6lem2  42144  aks5lem2  42160  evlsbagval  42539  selvvvval  42558  evlselv  42560  selvadd  42561  prjcrv0  42606