Theorem flddrngd 20661

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

Syntax hints:   → wi 4   ∈ wcel 2109  CRingccrg 20154  DivRingcdr 20649  Fieldcfield 20650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-in 3918  df-field 20652

This theorem is referenced by:  ply1asclunit  33536  ply1unit  33537  ply1dg1rt  33541  m1pmeq  33545  fldextsdrg  33643  fldgenfldext  33656  evls1fldgencl  33658  fldextrspunlsplem  33661  fldextrspunfld  33664  fldextrspunlem2  33665  fldextrspundgdvdslem  33668  fldextrspundgdvds  33669  minplyirred  33694  algextdeglem2  33701  algextdeglem3  33702  algextdeglem4  33703  algextdeglem5  33704  algextdeglem7  33706  algextdeglem8  33707  rtelextdg2lem  33709  rtelextdg2  33710  constrsdrg  33758  aks6d1c5lem3  42118  aks6d1c5lem2  42119  aks5lem7  42181  prjcrv0  42614