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 3446  df-in 3918  df-field 20617

This theorem is referenced by:  ply1asclunit  33516  ply1unit  33517  ply1dg1rt  33521  m1pmeq  33525  fldextsdrg  33623  fldgenfldext  33636  evls1fldgencl  33638  fldextrspunlsplem  33641  fldextrspunfld  33644  fldextrspunlem2  33645  fldextrspundgdvdslem  33648  fldextrspundgdvds  33649  minplyirred  33674  algextdeglem2  33681  algextdeglem3  33682  algextdeglem4  33683  algextdeglem5  33684  algextdeglem7  33686  algextdeglem8  33687  rtelextdg2lem  33689  rtelextdg2  33690  constrsdrg  33738  aks6d1c5lem3  42098  aks6d1c5lem2  42099  aks5lem7  42161  prjcrv0  42594