Theorem drngringd 20705

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

Syntax hints:   → wi 4   ∈ wcel 2107  Ringcrg 20198  DivRingcdr 20697

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3420  df-v 3465  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 4888  df-br 5124  df-iota 6494  df-fv 6549  df-drng 20699

This theorem is referenced by:  drnggrpd  20706  imadrhmcl  20766  frlmphl  21755  sdrgdvcl  33241  fldgensdrg  33256  primefldgen1  33263  ply1lvec  33520  m1pmeq  33543  ig1pnunit  33556  ig1pmindeg  33557  rlmdim  33595  ply1degltdimlem  33608  ply1degltdim  33609  fldgenfldext  33655  fldextrspunlsplem  33660  fldextrspunfld  33663  fldextrspunlem2  33664  fldextrspundgdvdslem  33667  fldextrspundgdvds  33668  irngnzply1lem  33677  minplyirredlem  33690  minplym1p  33693  minplynzm1p  33694  irredminply  33696  algextdeglem4  33700  algextdeglem7  33703  algextdeglem8  33704  2sqr3minply  33749  drnginvmuld  42500  prjspner1  42599