Theorem flddrngd 20674

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

Syntax hints:   → wi 4   ∈ wcel 2113  CRingccrg 20169  DivRingcdr 20662  Fieldcfield 20663

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 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-in 3908  df-field 20665

This theorem is referenced by:  ply1asclunit  33655  ply1unit  33656  ply1dg1rt  33661  m1pmeq  33666  fldextsdrg  33811  fldgenfldext  33825  evls1fldgencl  33827  fldextrspunlsplem  33830  fldextrspunfld  33833  fldextrspunlem2  33834  fldextrspundgdvdslem  33837  fldextrspundgdvds  33838  extdgfialglem1  33849  minplyirred  33868  algextdeglem2  33875  algextdeglem3  33876  algextdeglem4  33877  algextdeglem5  33878  algextdeglem7  33880  algextdeglem8  33881  rtelextdg2lem  33883  rtelextdg2  33884  constrsdrg  33932  aks6d1c5lem3  42391  aks6d1c5lem2  42392  aks5lem7  42454  prjcrv0  42876