Theorem drngringd 20670

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

Syntax hints:   → wi 4   ∈ wcel 2113  Ringcrg 20168  DivRingcdr 20662

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-drng 20664

This theorem is referenced by:  drnggrpd  20671  imadrhmcl  20730  frlmphl  21736  sdrgdvcl  33381  fldgensdrg  33396  primefldgen1  33403  ply1lvec  33640  m1pmeq  33666  ig1pnunit  33682  ig1pmindeg  33683  rlmdim  33766  ply1degltdimlem  33779  ply1degltdim  33780  fldgenfldext  33825  fldextrspunlsplem  33830  fldextrspunfld  33833  fldextrspunlem2  33834  fldextrspundgdvdslem  33837  fldextrspundgdvds  33838  irngnzply1lem  33847  minplyirredlem  33867  minplym1p  33870  minplynzm1p  33871  irredminply  33873  algextdeglem4  33877  algextdeglem7  33880  algextdeglem8  33881  constrsdrg  33932  2sqr3minply  33937  cos9thpiminplylem6  33944  cos9thpiminply  33945  drnginvmuld  42782  prjspner1  42869