Theorem flddrngd 20841

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

Syntax hints:   → wi 4   ∈ wcel 2143  CRingccrg 20311  DivRingcdr 20827  Fieldcfield 20828

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-in 3912  df-field 20830

This theorem is referenced by:  fldlring  33789  ply1asclunit  33864  ply1unit  33865  ply1dg1rt  33870  m1pmeq  33875  fldextsdrg  34044  fldgenfldext  34058  evls1fldgencl  34060  fldextrspunlsplem  34063  fldextrspunfld  34066  fldextrspunlem2  34067  fldextrspundgdvdslem  34070  fldextrspundgdvds  34071  extdgfialglem1  34082  minplyirred  34101  algextdeglem2  34108  algextdeglem3  34109  algextdeglem4  34110  algextdeglem5  34111  algextdeglem7  34113  algextdeglem8  34114  rtelextdg2lem  34116  rtelextdg2  34117  constrsdrg  34165  aks6d1c5lem3  42904  aks6d1c5lem2  42905  aks5lem7  42967  prjcrv0  43365