Theorem ringgrpd 20269

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

Syntax hints:   → wi 4   ∈ wcel 2108  Grpcgrp 18973  Ringcrg 20260

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-nul 5324

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rab 3444  df-v 3490  df-sbc 3805  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451  df-ring 20262

This theorem is referenced by:  crnggrpd  20274  ringcom  20303  lringuplu  20570  isdomn4  20738  drnggrpd  20760  lssvnegcl  20977  rngqiprngimfo  21334  rngqiprngfulem4  21347  asclmulg  21945  psrdi  22008  psrdir  22009  evlslem1  22129  mhplss  22182  evls1addd  22396  evls1maprhm  22401  rhmcomulmpl  22407  rhmmpl  22408  r1pid2  26221  ringdi22  33211  erler  33237  rlocmulval  33241  rloccring  33242  fracfld  33275  ofldchr  33309  znfermltl  33359  qsdrngilem  33487  qsdrngi  33488  qsdrnglem2  33489  qsdrng  33490  evls1subd  33562  q1pdir  33588  r1pcyc  33592  r1padd1  33593  r1pid2OLD  33594  r1plmhm  33595  r1pquslmic  33596  assalactf1o  33648  irredminply  33707  algextdeglem8  33715  rtelextdg2lem  33717  2sqr3minply  33738  ellcsrspsn  35609  ply1divalg3  35610  r1peuqusdeg1  35611  fldhmf1  42047  aks6d1c1p2  42066  aks6d1c5lem3  42094  aks5lem2  42144  aks5lem5a  42148  rhmcomulpsr  42506  rhmpsr  42507  evlsmaprhm  42525