Theorem drngringd 20702

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

Syntax hints:   → wi 4   ∈ wcel 2109  Ringcrg 20198  DivRingcdr 20694

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 2708

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 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-iota 6489  df-fv 6544  df-drng 20696

This theorem is referenced by:  drnggrpd  20703  imadrhmcl  20762  frlmphl  21746  sdrgdvcl  33298  fldgensdrg  33313  primefldgen1  33320  ply1lvec  33577  m1pmeq  33601  ig1pnunit  33615  ig1pmindeg  33616  rlmdim  33654  ply1degltdimlem  33667  ply1degltdim  33668  fldgenfldext  33714  fldextrspunlsplem  33719  fldextrspunfld  33722  fldextrspunlem2  33723  fldextrspundgdvdslem  33726  fldextrspundgdvds  33727  irngnzply1lem  33736  minplyirredlem  33749  minplym1p  33752  minplynzm1p  33753  irredminply  33755  algextdeglem4  33759  algextdeglem7  33762  algextdeglem8  33763  constrsdrg  33814  2sqr3minply  33819  cos9thpiminplylem6  33826  cos9thpiminply  33827  drnginvmuld  42517  prjspner1  42616