Theorem crnggrpd 20474

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Grpcgrp 19144  CRingccrg 20460

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 2733  ax-nul 5260

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 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rab 3414  df-v 3453  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 6494  df-fv 6546  df-ov 7423  df-ring 20461  df-cring 20462

This theorem is used by:  fermltlchr  21835  selvvvval  22451  selvadd  22452  psdmul  22487  psd1  22488  psdpw  22491  ply1chr  22624  ply1fermltlchr  22630  elrgspnsubrunlem1  33808  elrgspnsubrunlem2  33809  erlbr2d  33825  rlocaddval  33830  rloccring  33832  rloc0g  33833  rlocf1  33835  fracerl  33868  gsumind  33906  dflringlem2  34027  ressply1evls1  34097  evl1deg1  34108  evl1deg2  34109  evl1deg3  34110  ply1dg1rt  34112  vr1nz  34125  mplasclco  34148  psrmonprod  34184  mplmonprod  34186  esplyfvn  34209  irngss  34319  extdgfialglem1  34324  irredminply  34348  algextdeglem4  34352  algextdeglem5  34353  aks6d1c1p3  43160  aks6d1c2lem4  43177  aks6d1c6lem2  43221  aks5lem2  43237  evlsbagval  43614  evlselv  43617  prjcrv0  43669