Theorem flddrngd 20994

Description: A field is a division ring. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised 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 20993	. . 3 ⊢ (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing))
3	2	simplbi 502	. 2 ⊢ (𝑅 ∈ Field → 𝑅 ∈ DivRing)
4	1, 3	syl 18	1 ⊢ (𝜑 → 𝑅 ∈ DivRing)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  CRingccrg 20460  DivRingcdr 20980  Fieldcfield 20981

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-in 3906  df-field 20983

This theorem is used by:  fldlring  34031  ply1asclunit  34106  ply1unit  34107  ply1dg1rt  34112  m1pmeq  34117  fldextsdrg  34286  fldgenfldext  34300  evls1fldgencl  34302  fldextrspunlsplem  34305  fldextrspunfld  34308  fldextrspunlem2  34309  fldextrspundgdvdslem  34312  fldextrspundgdvds  34313  extdgfialglem1  34324  minplyirred  34343  algextdeglem2  34350  algextdeglem3  34351  algextdeglem4  34352  algextdeglem5  34353  algextdeglem7  34355  algextdeglem8  34356  rtelextdg2lem  34358  rtelextdg2  34359  constrsdrg  34407  aks6d1c5lem3  43187  aks6d1c5lem2  43188  aks5lem7  43250  prjcrv0  43669