Theorem flddrngd 20706

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 20705	. . 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 20199  DivRingcdr 20694  Fieldcfield 20695

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-in 3938  df-field 20697

This theorem is referenced by:  ply1asclunit  33592  ply1unit  33593  ply1dg1rt  33597  m1pmeq  33601  fldextsdrg  33701  fldgenfldext  33714  evls1fldgencl  33716  fldextrspunlsplem  33719  fldextrspunfld  33722  fldextrspunlem2  33723  fldextrspundgdvdslem  33726  fldextrspundgdvds  33727  minplyirred  33750  algextdeglem2  33757  algextdeglem3  33758  algextdeglem4  33759  algextdeglem5  33760  algextdeglem7  33762  algextdeglem8  33763  rtelextdg2lem  33765  rtelextdg2  33766  constrsdrg  33814  aks6d1c5lem3  42155  aks6d1c5lem2  42156  aks5lem7  42218  prjcrv0  42623