Theorem fldcrngd 20707

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

Syntax hints:   → wi 4   ∈ wcel 2109  CRingccrg 20199  DivRingcdr 20694  Fieldcfield 20695

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-in 3938  df-field 20697

This theorem is referenced by:  resrng  21586  frlmphl  21746  zringfrac  33574  ply1asclunit  33592  ply1unit  33593  ply1dg1rt  33597  ply1dg3rt0irred  33600  fldgenfldext  33714  evls1fldgencl  33716  fldextrspunlsp  33720  irngnzply1lem  33736  irngnzply1  33737  ply1annig1p  33743  minplycl  33745  ply1annprmidl  33746  minplymindeg  33747  minplyann  33748  minplyirredlem  33749  minplyirred  33750  irngnminplynz  33751  minplym1p  33752  minplynzm1p  33753  minplyelirng  33754  irredminply  33755  algextdeglem1  33756  algextdeglem2  33757  algextdeglem3  33758  algextdeglem4  33759  algextdeglem5  33760  algextdeglem6  33761  algextdeglem7  33762  algextdeglem8  33763  rtelextdg2lem  33765  2sqr3minply  33819  cos9thpiminply  33827  aks6d1c1p3  42128  aks6d1c1p4  42129  aks6d1c1p5  42130  aks6d1c1p7  42131  aks6d1c1p6  42132  aks6d1c1p8  42133  aks6d1c1  42134  aks6d1c2lem3  42144  aks6d1c2lem4  42145  aks6d1c5lem0  42153  aks6d1c5lem1  42154  aks6d1c5lem3  42155  aks6d1c5  42157  aks6d1c6lem1  42188  aks6d1c6lem2  42189  aks6d1c6lem3  42190  aks6d1c6lem4  42191  aks6d1c6lem5  42195  aks5lem1  42204  aks5lem2  42205  aks5lem3a  42207  aks5lem5a  42209  prjcrv0  42631