Theorem fldcrngd 20906

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  CRingccrg 20374  DivRingcdr 20891  Fieldcfield 20892

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-in 3906  df-field 20894

This theorem is used by:  resrng  21835  frlmphl  21995  gsumind  33786  fldlring  33910  zringfrac  33965  ply1asclunit  33985  ply1unit  33986  ply1dg1rt  33991  ply1dg3rt0irred  33995  psrmonprod  34063  esplyfvaln  34085  fldgenfldext  34179  evls1fldgencl  34181  fldextrspunlsp  34185  irngnzply1lem  34201  irngnzply1  34202  extdgfialglem1  34203  extdgfialglem2  34204  extdgfialg  34205  ply1annig1p  34215  minplycl  34217  ply1annprmidl  34218  minplymindeg  34219  minplyann  34220  minplyirredlem  34221  minplyirred  34222  irngnminplynz  34223  minplym1p  34224  minplynzm1p  34225  minplyelirng  34226  irredminply  34227  algextdeglem1  34228  algextdeglem2  34229  algextdeglem3  34230  algextdeglem4  34231  algextdeglem5  34232  algextdeglem6  34233  algextdeglem7  34234  algextdeglem8  34235  rtelextdg2lem  34237  2sqr3minply  34291  cos9thpiminply  34299  aks6d1c1p3  42977  aks6d1c1p4  42978  aks6d1c1p5  42979  aks6d1c1p7  42980  aks6d1c1p6  42981  aks6d1c1p8  42982  aks6d1c1  42983  aks6d1c2lem3  42993  aks6d1c2lem4  42994  aks6d1c5lem0  43002  aks6d1c5lem1  43003  aks6d1c5lem3  43004  aks6d1c5  43006  aks6d1c6lem1  43037  aks6d1c6lem2  43038  aks6d1c6lem3  43039  aks6d1c6lem4  43040  aks6d1c6lem5  43044  aks5lem1  43053  aks5lem2  43054  aks5lem3a  43056  aks5lem5a  43058  prjcrv0  43480