Theorem ringgrpd 20223

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 20219	. 2 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝑅 ∈ Grp)

Syntax hints:   → wi 4   ∈ wcel 2114  Grpcgrp 18909  Ringcrg 20214

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-nul 5241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rab 3390  df-v 3431  df-sbc 3729  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370  df-ring 20216

This theorem is referenced by:  crnggrpd  20228  ringcom  20261  lringuplu  20521  isdomn4  20693  drnggrpd  20715  lssvnegcl  20951  rngqiprngimfo  21299  rngqiprngfulem4  21312  ofldchr  21556  asclmulg  21882  psrdi  21943  psrdir  21944  evlslem1  22060  mhplss  22121  psdmvr  22135  evls1addd  22336  evls1maprhm  22341  rhmcomulmpl  22347  rhmmpl  22348  r1pid2  26127  gsummulsubdishift2  33130  ringdi22  33291  ringm1expp1  33295  elrgspnlem1  33303  elrgspnlem2  33304  elrgspnlem4  33306  elrgspn  33307  erler  33326  rlocmulval  33330  rloccring  33331  fracfld  33369  znfermltl  33426  qsdrngilem  33554  qsdrngi  33555  qsdrnglem2  33556  qsdrng  33557  evls1subd  33632  q1pdir  33663  r1pcyc  33667  r1padd1  33668  r1pid2OLD  33669  r1plmhm  33670  r1pquslmic  33671  mplmulmvr  33683  mplvrpmmhm  33690  psrgsum  33692  mplgsum  33697  esplyfval2  33709  esplyfval3  33716  esplyind  33719  vietalem  33723  vieta  33724  assalactf1o  33779  irredminply  33860  algextdeglem8  33868  rtelextdg2lem  33870  2sqr3minply  33924  cos9thpiminplylem6  33931  cos9thpiminply  33932  zrhcntr  34123  ellcsrspsn  35823  ply1divalg3  35824  r1peuqusdeg1  35825  fldhmf1  42529  aks6d1c1p2  42548  aks6d1c5lem3  42576  aks5lem2  42626  aks5lem5a  42630  rhmcomulpsr  42994  rhmpsr  42995  evlsmaprhm  43006