Theorem ringgrpd 20387

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Grpcgrp 19063  Ringcrg 20378

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 2147  ax-9 2155  ax-ext 2734  ax-nul 5267

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 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rab 3415  df-v 3455  df-sbc 3743  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-ov 7420  df-ring 20380

This theorem is used by:  crnggrpd  20392  ringdi22  20411  ringcom  20427  lringuplu  20712  isdomn4  20883  drnggrpd  20905  lssvnegcl  21146  rngqiprngimfo  21510  rngqiprngfulem4  21523  ofldchr  21795  asclmulg  22123  psrdi  22185  psrdir  22186  evlslem1  22304  rhmcomulmpl  22346  evlsmaprhm  22353  mhplss  22389  psdmvr  22403  evls1addd  22602  evls1maprhm  22607  rhmmpl  22611  r1pid2  26394  gsummulsubdishift2  33517  ringm1expp1  33681  elrgspnlem1  33690  elrgspnlem2  33691  elrgspnlem4  33693  elrgspn  33694  erler  33713  erld2  33714  rlocmulval  33718  rloccring  33719  fracfld  33757  znfermltl  33809  qsdrngilem  33904  qsdrngi  33905  qsdrnglem2  33906  qsdrng  33907  dflring2  33911  dflring3  33915  evls1subd  33990  q1pdir  34021  r1pcyc  34025  r1padd1  34026  r1plmhm  34027  r1pquslmic  34028  psrnzr  34030  0mplrim  34032  mplasclco  34034  selvply1rhmlem2  34039  selvply1rhmlem4  34041  selvply1rhm0  34044  mplmulmvr  34057  mplvrpmmhm  34064  psrgsum  34066  mplgsum  34071  esplyfval2  34083  esplyfval3  34090  esplyind  34093  vietalem  34097  vieta  34098  assalactf1o  34153  irredminply  34234  algextdeglem8  34242  rtelextdg2lem  34244  2sqr3minply  34298  cos9thpiminplylem6  34305  cos9thpiminply  34306  zrhcntr  34497  ellcsrspsn  36228  ply1divalg3  36229  r1peuqusdeg1  36230  fldhmf1  42964  aks6d1c1p2  42983  aks6d1c5lem3  43011  aks5lem2  43061  aks5lem5a  43065  rhmcomulpsr  43436  rhmpsr  43437  idomcanl  49270