Theorem ringgrpd 20502

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  Grpcgrp 19176  Ringcrg 20492

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-nul 5264

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rab 3417  df-v 3456  df-sbc 3743  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-iota 6515  df-fv 6569  df-ov 7449  df-ring 20494

This theorem is used by:  crnggrpd  20507  ringdi22  20526  ringcom  20542  lringuplu  20829  isdomn4  21000  drnggrpd  21022  lssvnegcl  21264  rngqiprngimfo  21630  rngqiprngfulem4  21643  ofldchr  21915  asclmulg  22243  psrdi  22305  psrdir  22306  psrring  22310  evlslem1  22424  rhmcomulmpl  22466  evlsmaprhm  22473  mhplss  22509  psdmvr  22523  evls1addd  22722  evls1maprhm  22727  rhmmpl  22731  r1pid2  26513  gsummulsubdishift2  33706  ringm1expp1  33870  elrgspnlem1  33879  elrgspnlem2  33880  elrgspnlem4  33882  elrgspn  33883  erler  33902  erld2  33903  rlocmulval  33907  rloccring  33908  fldedom  33937  edompidlem  33940  edompid  33941  fracfld  33954  znfermltl  34006  qsdrngilem  34102  qsdrngi  34103  qsdrnglem2  34104  qsdrng  34105  dflring2  34109  dflring3  34113  evls1subd  34187  q1pdir  34218  r1pcyc  34222  r1padd1  34223  r1plmhm  34224  r1pquslmic  34225  psrnzr  34227  0mplrim  34229  mplasclco  34231  selvply1rhmlem2  34236  selvply1rhmlem4  34238  selvply1rhm0  34241  mplmulmvr  34254  mplvrpmmhm  34261  psrgsum  34263  mplgsum  34268  esplyfval2  34280  esplyfval3  34287  esplyind  34290  vietalem  34294  vieta  34295  assalactf1o  34350  irredminply  34431  algextdeglem8  34439  rtelextdg2lem  34441  2sqr3minply  34495  cos9thpiminplylem6  34502  cos9thpiminply  34503  zrhcntr  34694  ellcsrspsn  36586  ply1divalg3  36587  r1peuqusdeg1  36588  fldhmf1  43343  aks6d1c1p2  43362  aks6d1c5lem3  43390  aks5lem2  43440  aks5lem5a  43444  rhmcomulpsr  43814  rhmpsr  43815  idomcanl  49659