Theorem flddrngd 21003

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 21002	. . 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 2144  CRingccrg 20469  DivRingcdr 20989  Fieldcfield 20990

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-in 4090  df-field 20992

This theorem is used by:  fldlring  34081  ply1asclunit  34156  ply1unit  34157  ply1dg1rt  34162  m1pmeq  34167  fldextsdrg  34336  fldgenfldext  34350  evls1fldgencl  34352  fldextrspunlsplem  34355  fldextrspunfld  34358  fldextrspunlem2  34359  fldextrspundgdvdslem  34362  fldextrspundgdvds  34363  extdgfialglem1  34374  minplyirred  34393  algextdeglem2  34400  algextdeglem3  34401  algextdeglem4  34402  algextdeglem5  34403  algextdeglem7  34405  algextdeglem8  34406  rtelextdg2lem  34408  rtelextdg2  34409  constrsdrg  34457  aks6d1c5lem3  43296  aks6d1c5lem2  43297  aks5lem7  43359  prjcrv0  43778