Theorem drngringd 20817

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

Syntax hints:   → wi 4   ∈ wcel 2149  Ringcrg 20311  DivRingcdr 20809

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-iota 6489  df-fv 6541  df-drng 20811

This theorem is referenced by:  drnggrpd  20818  imadrhmcl  20874  frlmphl  21896  sdrgdvcl  33559  fldgensdrg  33574  primefldgen1  33581  ply1lvec  33790  m1pmeq  33816  ig1pnunit  33832  ig1pmindeg  33833  rlmdim  33941  ply1degltdimlem  33953  ply1degltdim  33954  fldgenfldext  33999  fldextrspunlsplem  34004  fldextrspunfld  34007  fldextrspunlem2  34008  fldextrspundgdvdslem  34011  fldextrspundgdvds  34012  irngnzply1lem  34021  minplyirredlem  34041  minplym1p  34044  minplynzm1p  34045  irredminply  34047  algextdeglem4  34051  algextdeglem7  34054  algextdeglem8  34055  constrsdrg  34106  2sqr3minply  34111  cos9thpiminplylem6  34118  cos9thpiminply  34119  drnginvmuld  43180  prjspner1  43243