Theorem ringgrpd 20325

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

Syntax hints:   → wi 4   ∈ wcel 2143  Grpcgrp 19001  Ringcrg 20316

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-nul 5270

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rab 3417  df-v 3457  df-sbc 3746  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-iota 6494  df-fv 6546  df-ov 7415  df-ring 20318

This theorem is referenced by:  crnggrpd  20330  ringdi22  20348  ringcom  20364  lringuplu  20630  isdomn4  20801  drnggrpd  20823  lssvnegcl  21058  rngqiprngimfo  21422  rngqiprngfulem4  21435  ofldchr  21707  asclmulg  22033  psrdi  22095  psrdir  22096  evlslem1  22214  rhmcomulmpl  22256  evlsmaprhm  22263  mhplss  22299  psdmvr  22313  evls1addd  22512  evls1maprhm  22517  rhmmpl  22521  r1pid2  26300  gsummulsubdishift2  33370  ringm1expp1  33534  elrgspnlem1  33543  elrgspnlem2  33544  elrgspnlem4  33546  elrgspn  33547  erler  33566  erld2  33567  rlocmulval  33571  rloccring  33572  fracfld  33610  znfermltl  33662  qsdrngilem  33757  qsdrngi  33758  qsdrnglem2  33759  qsdrng  33760  dflring2  33764  dflring3  33768  evls1subd  33843  q1pdir  33874  r1pcyc  33878  r1padd1  33879  r1plmhm  33880  r1pquslmic  33881  psrnzr  33883  0mplrim  33885  mplasclco  33887  selvply1rhmlem2  33892  selvply1rhmlem4  33894  selvply1rhm0  33897  mplmulmvr  33910  mplvrpmmhm  33917  psrgsum  33919  mplgsum  33924  esplyfval2  33936  esplyfval3  33943  esplyind  33946  vietalem  33950  vieta  33951  assalactf1o  34006  irredminply  34087  algextdeglem8  34095  rtelextdg2lem  34097  2sqr3minply  34151  cos9thpiminplylem6  34158  cos9thpiminply  34159  zrhcntr  34350  ellcsrspsn  36114  ply1divalg3  36115  r1peuqusdeg1  36116  fldhmf1  42838  aks6d1c1p2  42857  aks6d1c5lem3  42885  aks5lem2  42935  aks5lem5a  42939  rhmcomulpsr  43297  rhmpsr  43298  idomcanl  49095