Theorem ringgrpd 20278

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

Syntax hints:   → wi 4   ∈ wcel 2141  Grpcgrp 18965  Ringcrg 20269

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-nul 5253

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3076  df-rab 3414  df-v 3455  df-sbc 3743  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-iota 6471  df-fv 6523  df-ov 7393  df-ring 20271

This theorem is referenced by:  crnggrpd  20283  ringcom  20316  lringuplu  20580  isdomn4  20752  drnggrpd  20774  lssvnegcl  21010  rngqiprngimfo  21358  rngqiprngfulem4  21371  ofldchr  21615  asclmulg  21941  psrdi  22003  psrdir  22004  evlslem1  22122  rhmcomulmpl  22164  evlsmaprhm  22171  mhplss  22207  psdmvr  22221  evls1addd  22421  evls1maprhm  22426  rhmmpl  22430  r1pid2  26209  gsummulsubdishift2  33209  ringdi22  33370  ringm1expp1  33374  elrgspnlem1  33383  elrgspnlem2  33384  elrgspnlem4  33386  elrgspn  33387  erler  33406  erld2  33407  rlocmulval  33411  rloccring  33412  fracfld  33455  znfermltl  33512  qsdrngilem  33642  qsdrngi  33643  qsdrnglem2  33644  qsdrng  33645  dflring2  33649  dflring3  33653  evls1subd  33728  q1pdir  33759  r1pcyc  33763  r1padd1  33764  r1pid2OLD  33765  r1plmhm  33766  r1pquslmic  33767  psrnzr  33769  0mplrim  33771  mplasclco  33773  selvply1rhmlem2  33778  selvply1rhmlem4  33780  selvply1rhm0  33783  mplmulmvr  33796  mplvrpmmhm  33803  psrgsum  33805  mplgsum  33810  esplyfval2  33822  esplyfval3  33829  esplyind  33832  vietalem  33836  vieta  33837  assalactf1o  33892  irredminply  33973  algextdeglem8  33981  rtelextdg2lem  33983  2sqr3minply  34037  cos9thpiminplylem6  34044  cos9thpiminply  34045  zrhcntr  34236  ellcsrspsn  35951  ply1divalg3  35952  r1peuqusdeg1  35953  fldhmf1  42667  aks6d1c1p2  42686  aks6d1c5lem3  42714  aks5lem2  42764  aks5lem5a  42768  rhmcomulpsr  43124  rhmpsr  43125