Theorem flddrngd 20904

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 20903	. . 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 2145  CRingccrg 20373  DivRingcdr 20890  Fieldcfield 20891

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-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-in 3906  df-field 20893

This theorem is used by:  fldlring  33909  ply1asclunit  33984  ply1unit  33985  ply1dg1rt  33990  m1pmeq  33995  fldextsdrg  34164  fldgenfldext  34178  evls1fldgencl  34180  fldextrspunlsplem  34183  fldextrspunfld  34186  fldextrspunlem2  34187  fldextrspundgdvdslem  34190  fldextrspundgdvds  34191  extdgfialglem1  34202  minplyirred  34221  algextdeglem2  34228  algextdeglem3  34229  algextdeglem4  34230  algextdeglem5  34231  algextdeglem7  34233  algextdeglem8  34234  rtelextdg2lem  34236  rtelextdg2  34237  constrsdrg  34285  aks6d1c5lem3  43003  aks6d1c5lem2  43004  aks5lem7  43066  prjcrv0  43479