Theorem ringgrpd 20151

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

Syntax hints:   → wi 4   ∈ wcel 2109  Grpcgrp 18865  Ringcrg 20142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5261

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rab 3406  df-v 3449  df-sbc 3754  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390  df-ring 20144

This theorem is referenced by:  crnggrpd  20156  ringcom  20189  lringuplu  20453  isdomn4  20625  drnggrpd  20647  lssvnegcl  20862  rngqiprngimfo  21211  rngqiprngfulem4  21224  asclmulg  21811  psrdi  21874  psrdir  21875  evlslem1  21989  mhplss  22042  psdmvr  22056  evls1addd  22258  evls1maprhm  22263  rhmcomulmpl  22269  rhmmpl  22270  r1pid2  26067  ringdi22  33182  elrgspnlem1  33193  elrgspnlem2  33194  elrgspnlem4  33196  elrgspn  33197  erler  33216  rlocmulval  33220  rloccring  33221  fracfld  33258  ofldchr  33292  znfermltl  33337  qsdrngilem  33465  qsdrngi  33466  qsdrnglem2  33467  qsdrng  33468  evls1subd  33541  q1pdir  33568  r1pcyc  33572  r1padd1  33573  r1pid2OLD  33574  r1plmhm  33575  r1pquslmic  33576  assalactf1o  33631  irredminply  33706  algextdeglem8  33714  rtelextdg2lem  33716  2sqr3minply  33770  cos9thpiminplylem6  33777  cos9thpiminply  33778  zrhcntr  33969  ellcsrspsn  35628  ply1divalg3  35629  r1peuqusdeg1  35630  fldhmf1  42078  aks6d1c1p2  42097  aks6d1c5lem3  42125  aks5lem2  42175  aks5lem5a  42179  rhmcomulpsr  42539  rhmpsr  42540  evlsmaprhm  42558