Theorem ringgrpd 20158

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

Syntax hints:   → wi 4   ∈ wcel 2109  Grpcgrp 18872  Ringcrg 20149

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 2702  ax-nul 5264

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 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rab 3409  df-v 3452  df-sbc 3757  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393  df-ring 20151

This theorem is referenced by:  crnggrpd  20163  ringcom  20196  lringuplu  20460  isdomn4  20632  drnggrpd  20654  lssvnegcl  20869  rngqiprngimfo  21218  rngqiprngfulem4  21231  asclmulg  21818  psrdi  21881  psrdir  21882  evlslem1  21996  mhplss  22049  psdmvr  22063  evls1addd  22265  evls1maprhm  22270  rhmcomulmpl  22276  rhmmpl  22277  r1pid2  26074  ringdi22  33189  elrgspnlem1  33200  elrgspnlem2  33201  elrgspnlem4  33203  elrgspn  33204  erler  33223  rlocmulval  33227  rloccring  33228  fracfld  33265  ofldchr  33299  znfermltl  33344  qsdrngilem  33472  qsdrngi  33473  qsdrnglem2  33474  qsdrng  33475  evls1subd  33548  q1pdir  33575  r1pcyc  33579  r1padd1  33580  r1pid2OLD  33581  r1plmhm  33582  r1pquslmic  33583  assalactf1o  33638  irredminply  33713  algextdeglem8  33721  rtelextdg2lem  33723  2sqr3minply  33777  cos9thpiminplylem6  33784  cos9thpiminply  33785  zrhcntr  33976  ellcsrspsn  35635  ply1divalg3  35636  r1peuqusdeg1  35637  fldhmf1  42085  aks6d1c1p2  42104  aks6d1c5lem3  42132  aks5lem2  42182  aks5lem5a  42186  rhmcomulpsr  42546  rhmpsr  42547  evlsmaprhm  42565