Theorem flddrngd 20787

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

Syntax hints:   → wi 4   ∈ wcel 2142  CRingccrg 20280  DivRingcdr 20775  Fieldcfield 20776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-in 3911  df-field 20778

This theorem is referenced by:  fldlring  33692  ply1asclunit  33767  ply1unit  33768  ply1dg1rt  33773  m1pmeq  33778  fldextsdrg  33948  fldgenfldext  33962  evls1fldgencl  33964  fldextrspunlsplem  33967  fldextrspunfld  33970  fldextrspunlem2  33971  fldextrspundgdvdslem  33974  fldextrspundgdvds  33975  extdgfialglem1  33986  minplyirred  34005  algextdeglem2  34012  algextdeglem3  34013  algextdeglem4  34014  algextdeglem5  34015  algextdeglem7  34017  algextdeglem8  34018  rtelextdg2lem  34020  rtelextdg2  34021  constrsdrg  34069  aks6d1c5lem3  42751  aks6d1c5lem2  42752  aks5lem7  42814  prjcrv0  43212