Theorem flddrngd 20713

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

Syntax hints:   → wi 4   ∈ wcel 2119  CRingccrg 20206  DivRingcdr 20701  Fieldcfield 20702

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-in 3890  df-field 20704

This theorem is referenced by:  ply1asclunit  33657  ply1unit  33658  ply1dg1rt  33663  m1pmeq  33668  fldextsdrg  33838  fldgenfldext  33852  evls1fldgencl  33854  fldextrspunlsplem  33857  fldextrspunfld  33860  fldextrspunlem2  33861  fldextrspundgdvdslem  33864  fldextrspundgdvds  33865  extdgfialglem1  33876  minplyirred  33895  algextdeglem2  33902  algextdeglem3  33903  algextdeglem4  33904  algextdeglem5  33905  algextdeglem7  33907  algextdeglem8  33908  rtelextdg2lem  33910  rtelextdg2  33911  constrsdrg  33959  aks6d1c5lem3  42622  aks6d1c5lem2  42623  aks5lem7  42685  prjcrv0  43083