Theorem ringgrpd 20143

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

Syntax hints:   → wi 4   ∈ wcel 2105  Grpcgrp 18861  Ringcrg 20134

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702  ax-nul 5306

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-ral 3061  df-rab 3432  df-v 3475  df-sbc 3778  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551  df-ov 7415  df-ring 20136

This theorem is referenced by:  crnggrpd  20148  ringcom  20175  lringuplu  20440  drnggrpd  20592  lssvnegcl  20799  rngqiprngimfo  21149  rngqiprngfulem4  21162  isdomn4  21207  psrdi  21837  psrdir  21838  evlslem1  21956  ofldchr  32869  znfermltl  32920  qsdrngilem  33049  qsdrngi  33050  qsdrnglem2  33051  qsdrng  33052  asclmulg  33076  evls1addd  33089  q1pdir  33115  r1pcyc  33119  r1padd1  33120  r1pid2  33121  r1plmhm  33122  r1pquslmic  33123  evls1maprhm  33215  algextdeglem8  33236  fldhmf1  41424  rhmcomulmpl  41589  rhmmpl  41590  evlsmaprhm  41607