Theorem ringgrpd 20312

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

Syntax hints:   → wi 4   ∈ wcel 2145  Grpcgrp 18988  Ringcrg 20303

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-nul 5260

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3080  df-rab 3418  df-v 3459  df-sbc 3748  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5105  df-iota 6481  df-fv 6533  df-ov 7403  df-ring 20305

This theorem is referenced by:  crnggrpd  20317  ringdi22  20335  ringcom  20351  lringuplu  20617  isdomn4  20788  drnggrpd  20810  lssvnegcl  21043  rngqiprngimfo  21400  rngqiprngfulem4  21413  ofldchr  21683  asclmulg  22009  psrdi  22071  psrdir  22072  evlslem1  22190  rhmcomulmpl  22232  evlsmaprhm  22239  mhplss  22275  psdmvr  22289  evls1addd  22488  evls1maprhm  22493  rhmmpl  22497  r1pid2  26276  gsummulsubdishift2  33297  ringm1expp1  33461  elrgspnlem1  33470  elrgspnlem2  33471  elrgspnlem4  33473  elrgspn  33474  erler  33493  erld2  33494  rlocmulval  33498  rloccring  33499  fracfld  33539  znfermltl  33591  qsdrngilem  33688  qsdrngi  33689  qsdrnglem2  33690  qsdrng  33691  dflring2  33695  dflring3  33699  evls1subd  33774  q1pdir  33805  r1pcyc  33809  r1padd1  33810  r1plmhm  33811  r1pquslmic  33812  psrnzr  33814  0mplrim  33816  mplasclco  33818  selvply1rhmlem2  33823  selvply1rhmlem4  33825  selvply1rhm0  33828  mplmulmvr  33841  mplvrpmmhm  33848  psrgsum  33850  mplgsum  33855  esplyfval2  33867  esplyfval3  33874  esplyind  33877  vietalem  33881  vieta  33882  assalactf1o  33937  irredminply  34018  algextdeglem8  34026  rtelextdg2lem  34028  2sqr3minply  34082  cos9thpiminplylem6  34089  cos9thpiminply  34090  zrhcntr  34281  ellcsrspsn  35999  ply1divalg3  36000  r1peuqusdeg1  36001  fldhmf1  42714  aks6d1c1p2  42733  aks6d1c5lem3  42761  aks5lem2  42811  aks5lem5a  42815  rhmcomulpsr  43171  rhmpsr  43172