Theorem flddrngd 20718

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

Syntax hints:   → wi 4   ∈ wcel 2114  CRingccrg 20215  DivRingcdr 20706  Fieldcfield 20707

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-in 3896  df-field 20709

This theorem is referenced by:  ply1asclunit  33634  ply1unit  33635  ply1dg1rt  33640  m1pmeq  33645  fldextsdrg  33798  fldgenfldext  33812  evls1fldgencl  33814  fldextrspunlsplem  33817  fldextrspunfld  33820  fldextrspunlem2  33821  fldextrspundgdvdslem  33824  fldextrspundgdvds  33825  extdgfialglem1  33836  minplyirred  33855  algextdeglem2  33862  algextdeglem3  33863  algextdeglem4  33864  algextdeglem5  33865  algextdeglem7  33867  algextdeglem8  33868  rtelextdg2lem  33870  rtelextdg2  33871  constrsdrg  33919  aks6d1c5lem3  42576  aks6d1c5lem2  42577  aks5lem7  42639  prjcrv0  43066