Theorem flddrngd 20650

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

Syntax hints:   → wi 4   ∈ wcel 2109  CRingccrg 20143  DivRingcdr 20638  Fieldcfield 20639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-in 3921  df-field 20641

This theorem is referenced by:  ply1asclunit  33543  ply1unit  33544  ply1dg1rt  33548  m1pmeq  33552  fldextsdrg  33650  fldgenfldext  33663  evls1fldgencl  33665  fldextrspunlsplem  33668  fldextrspunfld  33671  fldextrspunlem2  33672  fldextrspundgdvdslem  33675  fldextrspundgdvds  33676  minplyirred  33701  algextdeglem2  33708  algextdeglem3  33709  algextdeglem4  33710  algextdeglem5  33711  algextdeglem7  33713  algextdeglem8  33714  rtelextdg2lem  33716  rtelextdg2  33717  constrsdrg  33765  aks6d1c5lem3  42125  aks6d1c5lem2  42126  aks5lem7  42188  prjcrv0  42621