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 2111  Ringcrg 20152  DivRingcdr 20645

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-iota 6437  df-fv 6489  df-drng 20647

This theorem is referenced by:  drnggrpd  20654  imadrhmcl  20713  frlmphl  21719  sdrgdvcl  33263  fldgensdrg  33278  primefldgen1  33285  ply1lvec  33520  m1pmeq  33545  ig1pnunit  33559  ig1pmindeg  33560  rlmdim  33620  ply1degltdimlem  33633  ply1degltdim  33634  fldgenfldext  33679  fldextrspunlsplem  33684  fldextrspunfld  33687  fldextrspunlem2  33688  fldextrspundgdvdslem  33691  fldextrspundgdvds  33692  irngnzply1lem  33701  minplyirredlem  33721  minplym1p  33724  minplynzm1p  33725  irredminply  33727  algextdeglem4  33731  algextdeglem7  33734  algextdeglem8  33735  constrsdrg  33786  2sqr3minply  33791  cos9thpiminplylem6  33798  cos9thpiminply  33799  drnginvmuld  42566  prjspner1  42665