Theorem flddrngd 20891

Description: A field is a division ring. (Contributed by SN, 17-Jan-2025.)

Hypothesis

Ref	Expression
flddrngd.1	⊢ (𝜑 → 𝑅 ∈ Field)

Assertion

Ref	Expression
flddrngd	⊢ (𝜑 → 𝑅 ∈ DivRing)

Proof of Theorem flddrngd

Step	Hyp	Ref	Expression
1		flddrngd.1	. 2 ⊢ (𝜑 → 𝑅 ∈ Field)
2		isfld 20890	. . 3 ⊢ (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing))
3	2	simplbi 502	. 2 ⊢ (𝑅 ∈ Field → 𝑅 ∈ DivRing)
4	1, 3	syl 18	1 ⊢ (𝜑 → 𝑅 ∈ DivRing)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  CRingccrg 20360  DivRingcdr 20877  Fieldcfield 20878

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-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-in 3913  df-field 20880

This theorem is used by:  fldlring  33853  ply1asclunit  33928  ply1unit  33929  ply1dg1rt  33934  m1pmeq  33939  fldextsdrg  34108  fldgenfldext  34122  evls1fldgencl  34124  fldextrspunlsplem  34127  fldextrspunfld  34130  fldextrspunlem2  34131  fldextrspundgdvdslem  34134  fldextrspundgdvds  34135  extdgfialglem1  34146  minplyirred  34165  algextdeglem2  34172  algextdeglem3  34173  algextdeglem4  34174  algextdeglem5  34175  algextdeglem7  34177  algextdeglem8  34178  rtelextdg2lem  34180  rtelextdg2  34181  constrsdrg  34229  aks6d1c5lem3  42962  aks6d1c5lem2  42963  aks5lem7  43025  prjcrv0  43423