Theorem crnggrpd 20274

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

Syntax hints:   → wi 4   ∈ wcel 2108  Grpcgrp 18973  CRingccrg 20261

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-nul 5324

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rab 3444  df-v 3490  df-sbc 3805  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451  df-ring 20262  df-cring 20263

This theorem is referenced by:  fermltlchr  21567  psdmul  22193  psd1  22194  ply1chr  22331  ply1fermltlchr  22337  erlbr2d  33236  rlocaddval  33240  rloccring  33242  rloc0g  33243  rlocf1  33245  fracerl  33273  evl1deg1  33566  evl1deg2  33567  evl1deg3  33568  ply1dg1rt  33569  irngss  33687  irredminply  33707  algextdeglem4  33711  algextdeglem5  33712  aks6d1c1p3  42067  aks6d1c2lem4  42084  aks6d1c6lem2  42128  aks5lem2  42144  evlsbagval  42521  selvvvval  42540  evlselv  42542  selvadd  42543  prjcrv0  42588