Theorem ringgrpd 20145

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

Syntax hints:   → wi 4   ∈ wcel 2109  Grpcgrp 18830  Ringcrg 20136

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 5248

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 3397  df-v 3440  df-sbc 3745  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494  df-ov 7356  df-ring 20138

This theorem is referenced by:  crnggrpd  20150  ringcom  20183  lringuplu  20447  isdomn4  20619  drnggrpd  20641  lssvnegcl  20877  rngqiprngimfo  21226  rngqiprngfulem4  21239  ofldchr  21501  asclmulg  21827  psrdi  21890  psrdir  21891  evlslem1  22005  mhplss  22058  psdmvr  22072  evls1addd  22274  evls1maprhm  22279  rhmcomulmpl  22285  rhmmpl  22286  r1pid2  26083  ringdi22  33184  elrgspnlem1  33195  elrgspnlem2  33196  elrgspnlem4  33198  elrgspn  33199  erler  33218  rlocmulval  33222  rloccring  33223  fracfld  33260  znfermltl  33316  qsdrngilem  33444  qsdrngi  33445  qsdrnglem2  33446  qsdrng  33447  evls1subd  33520  q1pdir  33547  r1pcyc  33551  r1padd1  33552  r1pid2OLD  33553  r1plmhm  33554  r1pquslmic  33555  assalactf1o  33610  irredminply  33685  algextdeglem8  33693  rtelextdg2lem  33695  2sqr3minply  33749  cos9thpiminplylem6  33756  cos9thpiminply  33757  zrhcntr  33948  ellcsrspsn  35616  ply1divalg3  35617  r1peuqusdeg1  35618  fldhmf1  42066  aks6d1c1p2  42085  aks6d1c5lem3  42113  aks5lem2  42163  aks5lem5a  42167  rhmcomulpsr  42527  rhmpsr  42528  evlsmaprhm  42546