Theorem flddrngd 20672

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

Syntax hints:   → wi 4   ∈ wcel 2113  CRingccrg 20167  DivRingcdr 20660  Fieldcfield 20661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-in 3906  df-field 20663

This theorem is referenced by:  ply1asclunit  33604  ply1unit  33605  ply1dg1rt  33610  m1pmeq  33615  fldextsdrg  33760  fldgenfldext  33774  evls1fldgencl  33776  fldextrspunlsplem  33779  fldextrspunfld  33782  fldextrspunlem2  33783  fldextrspundgdvdslem  33786  fldextrspundgdvds  33787  extdgfialglem1  33798  minplyirred  33817  algextdeglem2  33824  algextdeglem3  33825  algextdeglem4  33826  algextdeglem5  33827  algextdeglem7  33829  algextdeglem8  33830  rtelextdg2lem  33832  rtelextdg2  33833  constrsdrg  33881  aks6d1c5lem3  42330  aks6d1c5lem2  42331  aks5lem7  42393  prjcrv0  42818