Theorem drngringd 20653

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

Syntax hints:   → wi 4   ∈ wcel 2109  Ringcrg 20149  DivRingcdr 20645

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-drng 20647

This theorem is referenced by:  drnggrpd  20654  imadrhmcl  20713  frlmphl  21697  sdrgdvcl  33256  fldgensdrg  33271  primefldgen1  33278  ply1lvec  33535  m1pmeq  33559  ig1pnunit  33573  ig1pmindeg  33574  rlmdim  33612  ply1degltdimlem  33625  ply1degltdim  33626  fldgenfldext  33670  fldextrspunlsplem  33675  fldextrspunfld  33678  fldextrspunlem2  33679  fldextrspundgdvdslem  33682  fldextrspundgdvds  33683  irngnzply1lem  33692  minplyirredlem  33707  minplym1p  33710  minplynzm1p  33711  irredminply  33713  algextdeglem4  33717  algextdeglem7  33720  algextdeglem8  33721  constrsdrg  33772  2sqr3minply  33777  cos9thpiminplylem6  33784  cos9thpiminply  33785  drnginvmuld  42522  prjspner1  42621