Theorem ringgrpd 20214

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

Syntax hints:   → wi 4   ∈ wcel 2114  Grpcgrp 18900  Ringcrg 20205

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 2709  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 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rab 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6448  df-fv 6500  df-ov 7363  df-ring 20207

This theorem is referenced by:  crnggrpd  20219  ringcom  20252  lringuplu  20512  isdomn4  20684  drnggrpd  20706  lssvnegcl  20942  rngqiprngimfo  21291  rngqiprngfulem4  21304  ofldchr  21566  asclmulg  21892  psrdi  21953  psrdir  21954  evlslem1  22070  mhplss  22131  psdmvr  22145  evls1addd  22346  evls1maprhm  22351  rhmcomulmpl  22357  rhmmpl  22358  r1pid2  26137  gsummulsubdishift2  33145  ringdi22  33306  ringm1expp1  33310  elrgspnlem1  33318  elrgspnlem2  33319  elrgspnlem4  33321  elrgspn  33322  erler  33341  rlocmulval  33345  rloccring  33346  fracfld  33384  znfermltl  33441  qsdrngilem  33569  qsdrngi  33570  qsdrnglem2  33571  qsdrng  33572  evls1subd  33647  q1pdir  33678  r1pcyc  33682  r1padd1  33683  r1pid2OLD  33684  r1plmhm  33685  r1pquslmic  33686  mplmulmvr  33698  mplvrpmmhm  33705  psrgsum  33707  mplgsum  33712  esplyfval2  33724  esplyfval3  33731  esplyind  33734  vietalem  33738  vieta  33739  assalactf1o  33795  irredminply  33876  algextdeglem8  33884  rtelextdg2lem  33886  2sqr3minply  33940  cos9thpiminplylem6  33947  cos9thpiminply  33948  zrhcntr  34139  ellcsrspsn  35839  ply1divalg3  35840  r1peuqusdeg1  35841  fldhmf1  42543  aks6d1c1p2  42562  aks6d1c5lem3  42590  aks5lem2  42640  aks5lem5a  42644  rhmcomulpsr  43008  rhmpsr  43009  evlsmaprhm  43020