Theorem ringgrpd 20355

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  Grpcgrp 19031  Ringcrg 20346

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-nul 5274

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 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ne 2962  df-ral 3083  df-rab 3420  df-v 3460  df-sbc 3748  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-iota 6499  df-fv 6551  df-ov 7426  df-ring 20348

This theorem is used by:  crnggrpd  20360  ringdi22  20379  ringcom  20395  lringuplu  20680  isdomn4  20851  drnggrpd  20873  lssvnegcl  21114  rngqiprngimfo  21478  rngqiprngfulem4  21491  ofldchr  21763  asclmulg  22089  psrdi  22151  psrdir  22152  evlslem1  22270  rhmcomulmpl  22312  evlsmaprhm  22319  mhplss  22355  psdmvr  22369  evls1addd  22568  evls1maprhm  22573  rhmmpl  22577  r1pid2  26356  gsummulsubdishift2  33420  ringm1expp1  33584  elrgspnlem1  33593  elrgspnlem2  33594  elrgspnlem4  33596  elrgspn  33597  erler  33616  erld2  33617  rlocmulval  33621  rloccring  33622  fracfld  33660  znfermltl  33712  qsdrngilem  33807  qsdrngi  33808  qsdrnglem2  33809  qsdrng  33810  dflring2  33814  dflring3  33818  evls1subd  33893  q1pdir  33924  r1pcyc  33928  r1padd1  33929  r1plmhm  33930  r1pquslmic  33931  psrnzr  33933  0mplrim  33935  mplasclco  33937  selvply1rhmlem2  33942  selvply1rhmlem4  33944  selvply1rhm0  33947  mplmulmvr  33960  mplvrpmmhm  33967  psrgsum  33969  mplgsum  33974  esplyfval2  33986  esplyfval3  33993  esplyind  33996  vietalem  34000  vieta  34001  assalactf1o  34056  irredminply  34137  algextdeglem8  34145  rtelextdg2lem  34147  2sqr3minply  34201  cos9thpiminplylem6  34208  cos9thpiminply  34209  zrhcntr  34400  ellcsrspsn  36154  ply1divalg3  36155  r1peuqusdeg1  36156  fldhmf1  42898  aks6d1c1p2  42917  aks6d1c5lem3  42945  aks5lem2  42995  aks5lem5a  42999  rhmcomulpsr  43355  rhmpsr  43356  idomcanl  49153