Theorem flddrngd 20987

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 20986	. . 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 20453  DivRingcdr 20973  Fieldcfield 20974

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 20976

This theorem is used by:  fldlring  34024  ply1asclunit  34099  ply1unit  34100  ply1dg1rt  34105  m1pmeq  34110  fldextsdrg  34279  fldgenfldext  34293  evls1fldgencl  34295  fldextrspunlsplem  34298  fldextrspunfld  34301  fldextrspunlem2  34302  fldextrspundgdvdslem  34305  fldextrspundgdvds  34306  extdgfialglem1  34317  minplyirred  34336  algextdeglem2  34343  algextdeglem3  34344  algextdeglem4  34345  algextdeglem5  34346  algextdeglem7  34348  algextdeglem8  34349  rtelextdg2lem  34351  rtelextdg2  34352  constrsdrg  34400  aks6d1c5lem3  43167  aks6d1c5lem2  43168  aks5lem7  43230  prjcrv0  43649