Theorem fldcrngd 20673

Description: A field is a commutative ring. (Contributed by SN, 23-Nov-2024.)

Hypothesis

Ref	Expression
fldcrngd.1	⊢ (𝜑 → 𝑅 ∈ Field)

Assertion

Ref	Expression
fldcrngd	⊢ (𝜑 → 𝑅 ∈ CRing)

Proof of Theorem fldcrngd

Step	Hyp	Ref	Expression
1		fldcrngd.1	. 2 ⊢ (𝜑 → 𝑅 ∈ Field)
2		isfld 20671	. . 3 ⊢ (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing))
3	2	simprbi 496	. 2 ⊢ (𝑅 ∈ Field → 𝑅 ∈ CRing)
4	1, 3	syl 17	1 ⊢ (𝜑 → 𝑅 ∈ CRing)

Syntax hints:   → wi 4   ∈ wcel 2113  CRingccrg 20167  DivRingcdr 20660  Fieldcfield 20661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-in 3906  df-field 20663

This theorem is referenced by:  resrng  21574  frlmphl  21734  gsumind  33375  zringfrac  33584  ply1asclunit  33604  ply1unit  33605  ply1dg1rt  33610  ply1dg3rt0irred  33614  fldgenfldext  33774  evls1fldgencl  33776  fldextrspunlsp  33780  irngnzply1lem  33796  irngnzply1  33797  extdgfialglem1  33798  extdgfialglem2  33799  extdgfialg  33800  ply1annig1p  33810  minplycl  33812  ply1annprmidl  33813  minplymindeg  33814  minplyann  33815  minplyirredlem  33816  minplyirred  33817  irngnminplynz  33818  minplym1p  33819  minplynzm1p  33820  minplyelirng  33821  irredminply  33822  algextdeglem1  33823  algextdeglem2  33824  algextdeglem3  33825  algextdeglem4  33826  algextdeglem5  33827  algextdeglem6  33828  algextdeglem7  33829  algextdeglem8  33830  rtelextdg2lem  33832  2sqr3minply  33886  cos9thpiminply  33894  aks6d1c1p3  42303  aks6d1c1p4  42304  aks6d1c1p5  42305  aks6d1c1p7  42306  aks6d1c1p6  42307  aks6d1c1p8  42308  aks6d1c1  42309  aks6d1c2lem3  42319  aks6d1c2lem4  42320  aks6d1c5lem0  42328  aks6d1c5lem1  42329  aks6d1c5lem3  42330  aks6d1c5  42332  aks6d1c6lem1  42363  aks6d1c6lem2  42364  aks6d1c6lem3  42365  aks6d1c6lem4  42366  aks6d1c6lem5  42370  aks5lem1  42379  aks5lem2  42380  aks5lem3a  42382  aks5lem5a  42384  prjcrv0  42818