Theorem fldcrngd 20825

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 20823	. . 3 ⊢ (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing))
3	2	simprbi 502	. 2 ⊢ (𝑅 ∈ Field → 𝑅 ∈ CRing)
4	1, 3	syl 18	1 ⊢ (𝜑 → 𝑅 ∈ CRing)

Syntax hints:   → wi 4   ∈ wcel 2149  CRingccrg 20315  DivRingcdr 20812  Fieldcfield 20813

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-in 3920  df-field 20815

This theorem is referenced by:  resrng  21739  frlmphl  21899  gsumind  33607  fldlring  33733  zringfrac  33788  ply1asclunit  33808  ply1unit  33809  ply1dg1rt  33814  ply1dg3rt0irred  33818  psrmonprod  33886  esplyfvaln  33908  fldgenfldext  34002  evls1fldgencl  34004  fldextrspunlsp  34008  irngnzply1lem  34024  irngnzply1  34025  extdgfialglem1  34026  extdgfialglem2  34027  extdgfialg  34028  ply1annig1p  34038  minplycl  34040  ply1annprmidl  34041  minplymindeg  34042  minplyann  34043  minplyirredlem  34044  minplyirred  34045  irngnminplynz  34046  minplym1p  34047  minplynzm1p  34048  minplyelirng  34049  irredminply  34050  algextdeglem1  34051  algextdeglem2  34052  algextdeglem3  34053  algextdeglem4  34054  algextdeglem5  34055  algextdeglem6  34056  algextdeglem7  34057  algextdeglem8  34058  rtelextdg2lem  34060  2sqr3minply  34114  cos9thpiminply  34122  aks6d1c1p3  42766  aks6d1c1p4  42767  aks6d1c1p5  42768  aks6d1c1p7  42769  aks6d1c1p6  42770  aks6d1c1p8  42771  aks6d1c1  42772  aks6d1c2lem3  42782  aks6d1c2lem4  42783  aks6d1c5lem0  42791  aks6d1c5lem1  42792  aks6d1c5lem3  42793  aks6d1c5  42795  aks6d1c6lem1  42826  aks6d1c6lem2  42827  aks6d1c6lem3  42828  aks6d1c6lem4  42829  aks6d1c6lem5  42833  aks5lem1  42842  aks5lem2  42843  aks5lem3a  42845  aks5lem5a  42847  prjcrv0  43256