Theorem drngringd 20646

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

Syntax hints:   → wi 4   ∈ wcel 2109  Ringcrg 20142  DivRingcdr 20638

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-drng 20640

This theorem is referenced by:  drnggrpd  20647  imadrhmcl  20706  frlmphl  21690  sdrgdvcl  33249  fldgensdrg  33264  primefldgen1  33271  ply1lvec  33528  m1pmeq  33552  ig1pnunit  33566  ig1pmindeg  33567  rlmdim  33605  ply1degltdimlem  33618  ply1degltdim  33619  fldgenfldext  33663  fldextrspunlsplem  33668  fldextrspunfld  33671  fldextrspunlem2  33672  fldextrspundgdvdslem  33675  fldextrspundgdvds  33676  irngnzply1lem  33685  minplyirredlem  33700  minplym1p  33703  minplynzm1p  33704  irredminply  33706  algextdeglem4  33710  algextdeglem7  33713  algextdeglem8  33714  constrsdrg  33765  2sqr3minply  33770  cos9thpiminplylem6  33777  cos9thpiminply  33778  drnginvmuld  42515  prjspner1  42614