Theorem ringgrpd 20161

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

Syntax hints:   → wi 4   ∈ wcel 2111  Grpcgrp 18846  Ringcrg 20152

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 2113  ax-9 2121  ax-ext 2703  ax-nul 5244

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 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rab 3396  df-v 3438  df-sbc 3742  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-iota 6437  df-fv 6489  df-ov 7349  df-ring 20154

This theorem is referenced by:  crnggrpd  20166  ringcom  20199  lringuplu  20460  isdomn4  20632  drnggrpd  20654  lssvnegcl  20890  rngqiprngimfo  21239  rngqiprngfulem4  21252  ofldchr  21514  asclmulg  21840  psrdi  21903  psrdir  21904  evlslem1  22018  mhplss  22071  psdmvr  22085  evls1addd  22287  evls1maprhm  22292  rhmcomulmpl  22298  rhmmpl  22299  r1pid2  26095  ringdi22  33196  elrgspnlem1  33207  elrgspnlem2  33208  elrgspnlem4  33210  elrgspn  33211  erler  33230  rlocmulval  33234  rloccring  33235  fracfld  33272  znfermltl  33329  qsdrngilem  33457  qsdrngi  33458  qsdrnglem2  33459  qsdrng  33460  evls1subd  33533  q1pdir  33561  r1pcyc  33565  r1padd1  33566  r1pid2OLD  33567  r1plmhm  33568  r1pquslmic  33569  mplvrpmmhm  33574  assalactf1o  33646  irredminply  33727  algextdeglem8  33735  rtelextdg2lem  33737  2sqr3minply  33791  cos9thpiminplylem6  33798  cos9thpiminply  33799  zrhcntr  33990  ellcsrspsn  35683  ply1divalg3  35684  r1peuqusdeg1  35685  fldhmf1  42129  aks6d1c1p2  42148  aks6d1c5lem3  42176  aks5lem2  42226  aks5lem5a  42230  rhmcomulpsr  42590  rhmpsr  42591  evlsmaprhm  42609