Theorem flddrngd 21045

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 21044	. . 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 2147  CRingccrg 20511  DivRingcdr 21031  Fieldcfield 21032

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-in 4094  df-field 21034

This theorem is used by:  fldedom  33956  ply1edom  33959  fldlring  34135  ply1asclunit  34209  ply1unit  34210  ply1dg1rt  34215  m1pmeq  34220  fldextsdrg  34397  fldgenfldext  34411  evls1fldgencl  34413  fldextrspunlsplem  34416  fldextrspunfld  34419  fldextrspunlem2  34420  fldextrspundgdvdslem  34423  fldextrspundgdvds  34424  extdgfialglem1  34435  minplyirred  34454  algextdeglem2  34461  algextdeglem3  34462  algextdeglem4  34463  algextdeglem5  34464  algextdeglem7  34466  algextdeglem8  34467  rtelextdg2lem  34469  rtelextdg2  34470  constrsdrg  34518  aks6d1c5lem3  43453  aks6d1c5lem2  43454  aks5lem7  43516  prjcrv0  43935