Theorem drngringd 20994

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  Ringcrg 20465  DivRingcdr 20986

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6547  df-drng 20988

This theorem is used by:  drnggrpd  20995  imadrhmcl  21060  frlmphl  22093  sdrgdvcl  33908  fldgensdrg  33923  primefldgen1  33930  ply1lvec  34138  m1pmeq  34164  ig1pnunit  34180  ig1pmindeg  34181  rlmdim  34289  ply1degltdimlem  34301  ply1degltdim  34302  fedgmul  34310  fldgenfldext  34347  fldextrspunlsplem  34352  fldextrspunfld  34355  fldextrspunlem2  34356  fldextrspundgdvdslem  34359  fldextrspundgdvds  34360  irngnzply1lem  34369  minplyirredlem  34389  minplym1p  34392  minplynzm1p  34393  irredminply  34395  algextdeglem4  34399  algextdeglem7  34402  algextdeglem8  34403  constrsdrg  34454  2sqr3minply  34459  cos9thpiminplylem6  34466  cos9thpiminply  34467  drnginvmuld  43682  frlmnzcoordsca  43752  prjspnequivnorm  43754  prjspnnorm  43755