Theorem ringgrpd 20132

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

Syntax hints:   → wi 4   ∈ wcel 2098  Grpcgrp 18850  Ringcrg 20123

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695  ax-nul 5296

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-ne 2933  df-ral 3054  df-rab 3425  df-v 3468  df-sbc 3770  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-nul 4315  df-if 4521  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-br 5139  df-iota 6485  df-fv 6541  df-ov 7404  df-ring 20125

This theorem is referenced by:  crnggrpd  20137  ringcom  20164  lringuplu  20429  drnggrpd  20581  lssvnegcl  20788  rngqiprngimfo  21139  rngqiprngfulem4  21152  isdomn4  21197  psrdi  21827  psrdir  21828  evlslem1  21946  ofldchr  32859  znfermltl  32910  qsdrngilem  33039  qsdrngi  33040  qsdrnglem2  33041  qsdrng  33042  asclmulg  33066  evls1addd  33079  q1pdir  33105  r1pcyc  33109  r1padd1  33110  r1pid2  33111  r1plmhm  33112  r1pquslmic  33113  evls1maprhm  33205  algextdeglem8  33226  fldhmf1  41414  rhmcomulmpl  41579  rhmmpl  41580  evlsmaprhm  41597