Theorem ringgrpd 20221

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

Syntax hints:   → wi 4   ∈ wcel 2119  Grpcgrp 18907  Ringcrg 20212

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-nul 5235

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-ral 3055  df-rab 3393  df-v 3434  df-sbc 3731  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-iota 6448  df-fv 6500  df-ov 7366  df-ring 20214

This theorem is referenced by:  crnggrpd  20226  ringcom  20259  lringuplu  20523  isdomn4  20695  drnggrpd  20717  lssvnegcl  20953  rngqiprngimfo  21301  rngqiprngfulem4  21314  ofldchr  21558  asclmulg  21884  psrdi  21946  psrdir  21947  evlslem1  22065  rhmcomulmpl  22107  evlsmaprhm  22114  mhplss  22150  psdmvr  22164  evls1addd  22364  evls1maprhm  22369  rhmmpl  22373  r1pid2  26152  gsummulsubdishift2  33157  ringdi22  33318  ringm1expp1  33322  elrgspnlem1  33330  elrgspnlem2  33331  elrgspnlem4  33333  elrgspn  33334  erler  33353  rlocmulval  33357  rloccring  33358  fracfld  33399  znfermltl  33456  qsdrngilem  33584  qsdrngi  33585  qsdrnglem2  33586  qsdrng  33587  evls1subd  33662  q1pdir  33693  r1pcyc  33697  r1padd1  33698  r1pid2OLD  33699  r1plmhm  33700  r1pquslmic  33701  psrnzr  33703  0mplrim  33705  mplasclco  33707  selvply1rhmlem2  33712  selvply1rhmlem4  33714  selvply1rhm0  33717  mplmulmvr  33730  mplvrpmmhm  33737  psrgsum  33739  mplgsum  33744  esplyfval2  33756  esplyfval3  33763  esplyind  33766  vietalem  33770  vieta  33771  assalactf1o  33826  irredminply  33907  algextdeglem8  33915  rtelextdg2lem  33917  2sqr3minply  33971  cos9thpiminplylem6  33978  cos9thpiminply  33979  zrhcntr  34170  ellcsrspsn  35876  ply1divalg3  35877  r1peuqusdeg1  35878  fldhmf1  42582  aks6d1c1p2  42601  aks6d1c5lem3  42629  aks5lem2  42679  aks5lem5a  42683  rhmcomulpsr  43039  rhmpsr  43040