Theorem drngringd 20716

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

Syntax hints:   → wi 4   ∈ wcel 2119  Ringcrg 20212  DivRingcdr 20708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-iota 6448  df-fv 6500  df-drng 20710

This theorem is referenced by:  drnggrpd  20717  imadrhmcl  20776  frlmphl  21763  sdrgdvcl  33390  fldgensdrg  33405  primefldgen1  33412  ply1lvec  33649  m1pmeq  33675  ig1pnunit  33691  ig1pmindeg  33692  rlmdim  33801  ply1degltdimlem  33813  ply1degltdim  33814  fldgenfldext  33859  fldextrspunlsplem  33864  fldextrspunfld  33867  fldextrspunlem2  33868  fldextrspundgdvdslem  33871  fldextrspundgdvds  33872  irngnzply1lem  33881  minplyirredlem  33901  minplym1p  33904  minplynzm1p  33905  irredminply  33907  algextdeglem4  33911  algextdeglem7  33914  algextdeglem8  33915  constrsdrg  33966  2sqr3minply  33971  cos9thpiminplylem6  33978  cos9thpiminply  33979  drnginvmuld  43020  prjspner1  43083