Theorem flddrngd 20626

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 20625	. . 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 20119  DivRingcdr 20614  Fieldcfield 20615

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 3438  df-in 3910  df-field 20617

This theorem is referenced by:  ply1asclunit  33509  ply1unit  33510  ply1dg1rt  33515  m1pmeq  33519  fldextsdrg  33621  fldgenfldext  33635  evls1fldgencl  33637  fldextrspunlsplem  33640  fldextrspunfld  33643  fldextrspunlem2  33644  fldextrspundgdvdslem  33647  fldextrspundgdvds  33648  extdgfialglem1  33659  minplyirred  33678  algextdeglem2  33685  algextdeglem3  33686  algextdeglem4  33687  algextdeglem5  33688  algextdeglem7  33690  algextdeglem8  33691  rtelextdg2lem  33693  rtelextdg2  33694  constrsdrg  33742  aks6d1c5lem3  42110  aks6d1c5lem2  42111  aks5lem7  42173  prjcrv0  42606