Theorem flddrngd 20742

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

Syntax hints:   → wi 4   ∈ wcel 2107  CRingccrg 20232  DivRingcdr 20730  Fieldcfield 20731

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481  df-in 3957  df-field 20733

This theorem is referenced by:  ply1asclunit  33600  ply1unit  33601  ply1dg1rt  33605  m1pmeq  33609  fldgenfldext  33719  evls1fldgencl  33721  fldextrspunlsplem  33724  fldextrspunfld  33727  fldextrspunlem2  33728  fldextrspundgdvdslem  33731  fldextrspundgdvds  33732  minplyirred  33755  algextdeglem2  33760  algextdeglem3  33761  algextdeglem4  33762  algextdeglem5  33763  algextdeglem7  33765  algextdeglem8  33766  rtelextdg2lem  33768  rtelextdg2  33769  aks6d1c5lem3  42139  aks6d1c5lem2  42140  aks5lem7  42202  prjcrv0  42648