Theorem drngringd 20864

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  Ringcrg 20338  DivRingcdr 20856

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-drng 20858

This theorem is used by:  drnggrpd  20865  imadrhmcl  20929  frlmphl  21960  sdrgdvcl  33643  fldgensdrg  33658  primefldgen1  33665  ply1lvec  33872  m1pmeq  33898  ig1pnunit  33914  ig1pmindeg  33915  rlmdim  34023  ply1degltdimlem  34035  ply1degltdim  34036  fldgenfldext  34081  fldextrspunlsplem  34086  fldextrspunfld  34089  fldextrspunlem2  34090  fldextrspundgdvdslem  34093  fldextrspundgdvds  34094  irngnzply1lem  34103  minplyirredlem  34123  minplym1p  34126  minplynzm1p  34127  irredminply  34129  algextdeglem4  34133  algextdeglem7  34136  algextdeglem8  34137  constrsdrg  34188  2sqr3minply  34193  cos9thpiminplylem6  34200  cos9thpiminply  34201  drnginvmuld  43328  prjspner1  43391