Theorem drngringd 20898

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Ringcrg 20372  DivRingcdr 20890

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 2732

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  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 6489  df-fv 6541  df-drng 20892

This theorem is used by:  drnggrpd  20899  imadrhmcl  20963  frlmphl  21994  sdrgdvcl  33740  fldgensdrg  33755  primefldgen1  33762  ply1lvec  33969  m1pmeq  33995  ig1pnunit  34011  ig1pmindeg  34012  rlmdim  34120  ply1degltdimlem  34132  ply1degltdim  34133  fldgenfldext  34178  fldextrspunlsplem  34183  fldextrspunfld  34186  fldextrspunlem2  34187  fldextrspundgdvdslem  34190  fldextrspundgdvds  34191  irngnzply1lem  34200  minplyirredlem  34220  minplym1p  34223  minplynzm1p  34224  irredminply  34226  algextdeglem4  34230  algextdeglem7  34233  algextdeglem8  34234  constrsdrg  34285  2sqr3minply  34290  cos9thpiminplylem6  34297  cos9thpiminply  34298  drnginvmuld  43409  prjspner1  43472