Theorem flddrngd 20824

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

Syntax hints:   → wi 4   ∈ wcel 2149  CRingccrg 20315  DivRingcdr 20812  Fieldcfield 20813

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-in 3920  df-field 20815

This theorem is referenced by:  fldlring  33733  ply1asclunit  33808  ply1unit  33809  ply1dg1rt  33814  m1pmeq  33819  fldextsdrg  33988  fldgenfldext  34002  evls1fldgencl  34004  fldextrspunlsplem  34007  fldextrspunfld  34010  fldextrspunlem2  34011  fldextrspundgdvdslem  34014  fldextrspundgdvds  34015  extdgfialglem1  34026  minplyirred  34045  algextdeglem2  34052  algextdeglem3  34053  algextdeglem4  34054  algextdeglem5  34055  algextdeglem7  34057  algextdeglem8  34058  rtelextdg2lem  34060  rtelextdg2  34061  constrsdrg  34109  aks6d1c5lem3  42793  aks6d1c5lem2  42794  aks5lem7  42856  prjcrv0  43256