Theorem flddrngd 20656

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

Syntax hints:   → wi 4   ∈ wcel 2111  CRingccrg 20152  DivRingcdr 20644  Fieldcfield 20645

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-in 3904  df-field 20647

This theorem is referenced by:  ply1asclunit  33537  ply1unit  33538  ply1dg1rt  33543  m1pmeq  33547  fldextsdrg  33667  fldgenfldext  33681  evls1fldgencl  33683  fldextrspunlsplem  33686  fldextrspunfld  33689  fldextrspunlem2  33690  fldextrspundgdvdslem  33693  fldextrspundgdvds  33694  extdgfialglem1  33705  minplyirred  33724  algextdeglem2  33731  algextdeglem3  33732  algextdeglem4  33733  algextdeglem5  33734  algextdeglem7  33736  algextdeglem8  33737  rtelextdg2lem  33739  rtelextdg2  33740  constrsdrg  33788  aks6d1c5lem3  42178  aks6d1c5lem2  42179  aks5lem7  42241  prjcrv0  42674