Theorem ringgrpd 20181

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

Syntax hints:   → wi 4   ∈ wcel 2114  Grpcgrp 18867  Ringcrg 20172

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 6446  df-fv 6498  df-ov 7361  df-ring 20174

This theorem is referenced by:  crnggrpd  20186  ringcom  20219  lringuplu  20479  isdomn4  20651  drnggrpd  20673  lssvnegcl  20909  rngqiprngimfo  21258  rngqiprngfulem4  21271  ofldchr  21533  asclmulg  21859  psrdi  21921  psrdir  21922  evlslem1  22038  mhplss  22099  psdmvr  22113  evls1addd  22314  evls1maprhm  22319  rhmcomulmpl  22325  rhmmpl  22326  r1pid2  26108  gsummulsubdishift2  33135  ringdi22  33296  ringm1expp1  33300  elrgspnlem1  33308  elrgspnlem2  33309  elrgspnlem4  33311  elrgspn  33312  erler  33331  rlocmulval  33335  rloccring  33336  fracfld  33374  znfermltl  33431  qsdrngilem  33559  qsdrngi  33560  qsdrnglem2  33561  qsdrng  33562  evls1subd  33637  q1pdir  33668  r1pcyc  33672  r1padd1  33673  r1pid2OLD  33674  r1plmhm  33675  r1pquslmic  33676  mplmulmvr  33688  mplvrpmmhm  33695  psrgsum  33697  mplgsum  33702  esplyfval2  33714  esplyfval3  33721  esplyind  33724  vietalem  33728  vieta  33729  assalactf1o  33785  irredminply  33866  algextdeglem8  33874  rtelextdg2lem  33876  2sqr3minply  33930  cos9thpiminplylem6  33937  cos9thpiminply  33938  zrhcntr  34129  ellcsrspsn  35829  ply1divalg3  35830  r1peuqusdeg1  35831  fldhmf1  42521  aks6d1c1p2  42540  aks6d1c5lem3  42568  aks5lem2  42618  aks5lem5a  42622  rhmcomulpsr  42993  rhmpsr  42994  evlsmaprhm  43005