Theorem drngringd 20822

Description: A division ring is a ring. (Contributed by SN, 16-May-2024.)

Hypothesis

Ref	Expression
drngringd.1	⊢ (𝜑 → 𝑅 ∈ DivRing)

Assertion

Ref	Expression
drngringd	⊢ (𝜑 → 𝑅 ∈ Ring)

Proof of Theorem drngringd

Step	Hyp	Ref	Expression
1		drngringd.1	. 2 ⊢ (𝜑 → 𝑅 ∈ DivRing)
2		drngring 20821	. 2 ⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring)
3	1, 2	syl 18	1 ⊢ (𝜑 → 𝑅 ∈ Ring)

Syntax hints:   → wi 4   ∈ wcel 2143  Ringcrg 20316  DivRingcdr 20814

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-iota 6494  df-fv 6546  df-drng 20816

This theorem is referenced by:  drnggrpd  20823  imadrhmcl  20881  frlmphl  21912  sdrgdvcl  33601  fldgensdrg  33616  primefldgen1  33623  ply1lvec  33830  m1pmeq  33856  ig1pnunit  33872  ig1pmindeg  33873  rlmdim  33981  ply1degltdimlem  33993  ply1degltdim  33994  fldgenfldext  34039  fldextrspunlsplem  34044  fldextrspunfld  34047  fldextrspunlem2  34048  fldextrspundgdvdslem  34051  fldextrspundgdvds  34052  irngnzply1lem  34061  minplyirredlem  34081  minplym1p  34084  minplynzm1p  34085  irredminply  34087  algextdeglem4  34091  algextdeglem7  34094  algextdeglem8  34095  constrsdrg  34146  2sqr3minply  34151  cos9thpiminplylem6  34158  cos9thpiminply  34159  drnginvmuld  43278  prjspner1  43341