Theorem ringgrpd 20189

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

Syntax hints:   → wi 4   ∈ wcel 2114  Grpcgrp 18875  Ringcrg 20180

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 5253

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 3402  df-v 3444  df-sbc 3743  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371  df-ring 20182

This theorem is referenced by:  crnggrpd  20194  ringcom  20227  lringuplu  20489  isdomn4  20661  drnggrpd  20683  lssvnegcl  20919  rngqiprngimfo  21268  rngqiprngfulem4  21281  ofldchr  21543  asclmulg  21870  psrdi  21932  psrdir  21933  evlslem1  22049  mhplss  22110  psdmvr  22124  evls1addd  22327  evls1maprhm  22332  rhmcomulmpl  22338  rhmmpl  22339  r1pid2  26135  gsummulsubdishift2  33162  ringdi22  33323  ringm1expp1  33327  elrgspnlem1  33335  elrgspnlem2  33336  elrgspnlem4  33338  elrgspn  33339  erler  33358  rlocmulval  33362  rloccring  33363  fracfld  33401  znfermltl  33458  qsdrngilem  33586  qsdrngi  33587  qsdrnglem2  33588  qsdrng  33589  evls1subd  33664  q1pdir  33695  r1pcyc  33699  r1padd1  33700  r1pid2OLD  33701  r1plmhm  33702  r1pquslmic  33703  mplmulmvr  33715  mplvrpmmhm  33722  psrgsum  33724  mplgsum  33729  esplyfval2  33741  esplyfval3  33748  esplyind  33751  vietalem  33755  vieta  33756  assalactf1o  33812  irredminply  33893  algextdeglem8  33901  rtelextdg2lem  33903  2sqr3minply  33957  cos9thpiminplylem6  33964  cos9thpiminply  33965  zrhcntr  34156  ellcsrspsn  35854  ply1divalg3  35855  r1peuqusdeg1  35856  fldhmf1  42457  aks6d1c1p2  42476  aks6d1c5lem3  42504  aks5lem2  42554  aks5lem5a  42558  rhmcomulpsr  42916  rhmpsr  42917  evlsmaprhm  42928