Theorem drngringd 20981

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Ringcrg 20452  DivRingcdr 20973

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 2147  ax-9 2155  ax-ext 2733

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 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6493  df-fv 6545  df-drng 20975

This theorem is used by:  drnggrpd  20982  imadrhmcl  21047  frlmphl  22080  sdrgdvcl  33854  fldgensdrg  33869  primefldgen1  33876  ply1lvec  34084  m1pmeq  34110  ig1pnunit  34126  ig1pmindeg  34127  rlmdim  34235  ply1degltdimlem  34247  ply1degltdim  34248  fldgenfldext  34293  fldextrspunlsplem  34298  fldextrspunfld  34301  fldextrspunlem2  34302  fldextrspundgdvdslem  34305  fldextrspundgdvds  34306  irngnzply1lem  34315  minplyirredlem  34335  minplym1p  34338  minplynzm1p  34339  irredminply  34341  algextdeglem4  34345  algextdeglem7  34348  algextdeglem8  34349  constrsdrg  34400  2sqr3minply  34405  cos9thpiminplylem6  34412  cos9thpiminply  34413  drnginvmuld  43568  frlmnzcoordsca  43638  prjspnequivnorm  43640  prjspnnorm  43641