Theorem crnggrpd 20525

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  Grpcgrp 19194  CRingccrg 20511

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-nul 5266

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rab 3417  df-v 3456  df-sbc 3743  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-iota 6520  df-fv 6574  df-ov 7454  df-ring 20512  df-cring 20513

This theorem is used by:  fermltlchr  21890  selvvvval  22506  selvadd  22507  psdmul  22542  psd1  22543  psdpw  22546  ply1chr  22679  ply1fermltlchr  22685  elrgspnsubrunlem1  33907  elrgspnsubrunlem2  33908  erlbr2d  33924  rlocaddval  33929  rloccring  33931  rloc0g  33932  rlocf1  33934  fracerl  33972  gsumind  34010  dflringlem2  34131  ressply1evls1  34200  evl1deg1  34211  evl1deg2  34212  evl1deg3  34213  ply1dg1rt  34215  vr1nz  34228  rngunsnply1chr2lem3  34252  mplasclco  34259  psrmonprod  34295  mplmonprod  34297  esplyfvn  34320  irngss  34430  extdgfialglem1  34435  irredminply  34459  algextdeglem4  34463  algextdeglem5  34464  aks6d1c1p3  43426  aks6d1c2lem4  43443  aks6d1c6lem2  43487  aks5lem2  43503  evlsbagval  43880  evlselv  43883  prjcrv0  43935