Theorem flddrngd 20763

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 20762	. . 3 ⊢ (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing))
3	2	simplbi 497	. 2 ⊢ (𝑅 ∈ Field → 𝑅 ∈ DivRing)
4	1, 3	syl 17	1 ⊢ (𝜑 → 𝑅 ∈ DivRing)

Syntax hints:   → wi 4   ∈ wcel 2108  CRingccrg 20261  DivRingcdr 20751  Fieldcfield 20752

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-in 3983  df-field 20754

This theorem is referenced by:  ply1asclunit  33564  ply1unit  33565  ply1dg1rt  33569  m1pmeq  33573  fldgenfldext  33678  evls1fldgencl  33680  minplyirred  33704  algextdeglem2  33709  algextdeglem3  33710  algextdeglem4  33711  algextdeglem5  33712  algextdeglem7  33714  algextdeglem8  33715  rtelextdg2lem  33717  rtelextdg2  33718  aks6d1c5lem3  42094  aks6d1c5lem2  42095  aks5lem7  42157  prjcrv0  42588