Theorem ringgrpd 20202

Description: A ring is a group. (Contributed by SN, 16-May-2024.)

Hypothesis

Ref	Expression
ringgrpd.1	⊢ (𝜑 → 𝑅 ∈ Ring)

Assertion

Ref	Expression
ringgrpd	⊢ (𝜑 → 𝑅 ∈ Grp)

Proof of Theorem ringgrpd

Step	Hyp	Ref	Expression
1		ringgrpd.1	. 2 ⊢ (𝜑 → 𝑅 ∈ Ring)
2		ringgrp 20198	. 2 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝑅 ∈ Grp)

Syntax hints:   → wi 4   ∈ wcel 2108  Grpcgrp 18916  Ringcrg 20193

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-nul 5276

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-ral 3052  df-rab 3416  df-v 3461  df-sbc 3766  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6484  df-fv 6539  df-ov 7408  df-ring 20195

This theorem is referenced by:  crnggrpd  20207  ringcom  20240  lringuplu  20504  isdomn4  20676  drnggrpd  20698  lssvnegcl  20913  rngqiprngimfo  21262  rngqiprngfulem4  21275  asclmulg  21862  psrdi  21925  psrdir  21926  evlslem1  22040  mhplss  22093  psdmvr  22107  evls1addd  22309  evls1maprhm  22314  rhmcomulmpl  22320  rhmmpl  22321  r1pid2  26119  ringdi22  33226  elrgspnlem1  33237  elrgspnlem2  33238  elrgspnlem4  33240  elrgspn  33241  erler  33260  rlocmulval  33264  rloccring  33265  fracfld  33302  ofldchr  33336  znfermltl  33381  qsdrngilem  33509  qsdrngi  33510  qsdrnglem2  33511  qsdrng  33512  evls1subd  33585  q1pdir  33612  r1pcyc  33616  r1padd1  33617  r1pid2OLD  33618  r1plmhm  33619  r1pquslmic  33620  assalactf1o  33675  irredminply  33750  algextdeglem8  33758  rtelextdg2lem  33760  2sqr3minply  33814  cos9thpiminplylem6  33821  cos9thpiminply  33822  zrhcntr  34010  ellcsrspsn  35663  ply1divalg3  35664  r1peuqusdeg1  35665  fldhmf1  42103  aks6d1c1p2  42122  aks6d1c5lem3  42150  aks5lem2  42200  aks5lem5a  42204  rhmcomulpsr  42574  rhmpsr  42575  evlsmaprhm  42593