Theorem ringgrpd 20177

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

Syntax hints:   → wi 4   ∈ wcel 2113  Grpcgrp 18863  Ringcrg 20168

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-nul 5251

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rab 3400  df-v 3442  df-sbc 3741  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361  df-ring 20170

This theorem is referenced by:  crnggrpd  20182  ringcom  20215  lringuplu  20477  isdomn4  20649  drnggrpd  20671  lssvnegcl  20907  rngqiprngimfo  21256  rngqiprngfulem4  21269  ofldchr  21531  asclmulg  21858  psrdi  21920  psrdir  21921  evlslem1  22037  mhplss  22098  psdmvr  22112  evls1addd  22315  evls1maprhm  22320  rhmcomulmpl  22326  rhmmpl  22327  r1pid2  26123  gsummulsubdishift2  33152  ringdi22  33312  ringm1expp1  33316  elrgspnlem1  33324  elrgspnlem2  33325  elrgspnlem4  33327  elrgspn  33328  erler  33347  rlocmulval  33351  rloccring  33352  fracfld  33390  znfermltl  33447  qsdrngilem  33575  qsdrngi  33576  qsdrnglem2  33577  qsdrng  33578  evls1subd  33653  q1pdir  33684  r1pcyc  33688  r1padd1  33689  r1pid2OLD  33690  r1plmhm  33691  r1pquslmic  33692  mplmulmvr  33704  mplvrpmmhm  33711  esplyfval2  33723  esplyfval3  33730  esplyind  33731  vietalem  33735  vieta  33736  assalactf1o  33792  irredminply  33873  algextdeglem8  33881  rtelextdg2lem  33883  2sqr3minply  33937  cos9thpiminplylem6  33944  cos9thpiminply  33945  zrhcntr  34136  ellcsrspsn  35835  ply1divalg3  35836  r1peuqusdeg1  35837  fldhmf1  42344  aks6d1c1p2  42363  aks6d1c5lem3  42391  aks5lem2  42441  aks5lem5a  42445  rhmcomulpsr  42804  rhmpsr  42805  evlsmaprhm  42816