Theorem ringgrpd 20475

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  Grpcgrp 19150  Ringcrg 20465

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-nul 5259

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rab 3413  df-v 3452  df-sbc 3739  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6547  df-ov 7424  df-ring 20467

This theorem is used by:  crnggrpd  20480  ringdi22  20499  ringcom  20515  lringuplu  20802  isdomn4  20973  drnggrpd  20995  lssvnegcl  21237  rngqiprngimfo  21603  rngqiprngfulem4  21616  ofldchr  21888  asclmulg  22216  psrdi  22278  psrdir  22279  psrring  22283  evlslem1  22397  rhmcomulmpl  22439  evlsmaprhm  22446  mhplss  22482  psdmvr  22496  evls1addd  22695  evls1maprhm  22700  rhmmpl  22704  r1pid2  26486  gsummulsubdishift2  33677  ringm1expp1  33841  elrgspnlem1  33850  elrgspnlem2  33851  elrgspnlem4  33853  elrgspn  33854  erler  33873  erld2  33874  rlocmulval  33878  rloccring  33879  fracfld  33917  znfermltl  33969  qsdrngilem  34065  qsdrngi  34066  qsdrnglem2  34067  qsdrng  34068  dflring2  34072  dflring3  34076  evls1subd  34151  q1pdir  34182  r1pcyc  34186  r1padd1  34187  r1plmhm  34188  r1pquslmic  34189  psrnzr  34191  0mplrim  34193  mplasclco  34195  selvply1rhmlem2  34200  selvply1rhmlem4  34202  selvply1rhm0  34205  mplmulmvr  34218  mplvrpmmhm  34225  psrgsum  34227  mplgsum  34232  esplyfval2  34244  esplyfval3  34251  esplyind  34254  vietalem  34258  vieta  34259  assalactf1o  34314  irredminply  34395  algextdeglem8  34403  rtelextdg2lem  34405  2sqr3minply  34459  cos9thpiminplylem6  34466  cos9thpiminply  34467  zrhcntr  34658  ellcsrspsn  36493  ply1divalg3  36494  r1peuqusdeg1  36495  fldhmf1  43234  aks6d1c1p2  43253  aks6d1c5lem3  43281  aks5lem2  43331  aks5lem5a  43335  rhmcomulpsr  43704  rhmpsr  43705  idomcanl  49538