Theorem fldcrngd 20743

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

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:  resrng  21640  frlmphl  21802  zringfrac  33583  ply1asclunit  33600  ply1unit  33601  ply1dg1rt  33605  ply1dg3rt0irred  33608  fldgenfldext  33719  evls1fldgencl  33721  fldextrspunlsp  33725  irngnzply1lem  33741  irngnzply1  33742  ply1annig1p  33748  minplycl  33750  ply1annprmidl  33751  minplymindeg  33752  minplyann  33753  minplyirredlem  33754  minplyirred  33755  irngnminplynz  33756  minplym1p  33757  irredminply  33758  algextdeglem1  33759  algextdeglem2  33760  algextdeglem3  33761  algextdeglem4  33762  algextdeglem5  33763  algextdeglem6  33764  algextdeglem7  33765  algextdeglem8  33766  rtelextdg2lem  33768  2sqr3minply  33792  aks6d1c1p3  42112  aks6d1c1p4  42113  aks6d1c1p5  42114  aks6d1c1p7  42115  aks6d1c1p6  42116  aks6d1c1p8  42117  aks6d1c1  42118  aks6d1c2lem3  42128  aks6d1c2lem4  42129  aks6d1c5lem0  42137  aks6d1c5lem1  42138  aks6d1c5lem3  42139  aks6d1c5  42141  aks6d1c6lem1  42172  aks6d1c6lem2  42173  aks6d1c6lem3  42174  aks6d1c6lem4  42175  aks6d1c6lem5  42179  aks5lem1  42188  aks5lem2  42189  aks5lem3a  42191  aks5lem5a  42193  prjcrv0  42648