Theorem ringgrpd 20259

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

Syntax hints:   → wi 4   ∈ wcel 2105  Grpcgrp 18963  Ringcrg 20250

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-nul 5311

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-rab 3433  df-v 3479  df-sbc 3791  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-ov 7433  df-ring 20252

This theorem is referenced by:  crnggrpd  20264  ringcom  20293  lringuplu  20560  isdomn4  20732  drnggrpd  20754  lssvnegcl  20971  rngqiprngimfo  21328  rngqiprngfulem4  21341  asclmulg  21939  psrdi  22002  psrdir  22003  evlslem1  22123  mhplss  22176  evls1addd  22390  evls1maprhm  22395  rhmcomulmpl  22401  rhmmpl  22402  r1pid2  26215  ringdi22  33220  elrgspnlem1  33231  elrgspnlem2  33232  elrgspnlem4  33234  erler  33251  rlocmulval  33255  rloccring  33256  fracfld  33289  ofldchr  33323  znfermltl  33373  qsdrngilem  33501  qsdrngi  33502  qsdrnglem2  33503  qsdrng  33504  evls1subd  33576  q1pdir  33602  r1pcyc  33606  r1padd1  33607  r1pid2OLD  33608  r1plmhm  33609  r1pquslmic  33610  assalactf1o  33662  irredminply  33721  algextdeglem8  33729  rtelextdg2lem  33731  2sqr3minply  33752  zrhcntr  33941  ellcsrspsn  35625  ply1divalg3  35626  r1peuqusdeg1  35627  fldhmf1  42071  aks6d1c1p2  42090  aks6d1c5lem3  42118  aks5lem2  42168  aks5lem5a  42172  rhmcomulpsr  42537  rhmpsr  42538  evlsmaprhm  42556