Theorem fldcrngd 20714

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

Syntax hints:   → wi 4   ∈ wcel 2119  CRingccrg 20206  DivRingcdr 20701  Fieldcfield 20702

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-in 3890  df-field 20704

This theorem is referenced by:  resrng  21596  frlmphl  21756  gsumind  33428  zringfrac  33637  ply1asclunit  33657  ply1unit  33658  ply1dg1rt  33663  ply1dg3rt0irred  33667  psrmonprod  33736  esplyfvaln  33758  fldgenfldext  33852  evls1fldgencl  33854  fldextrspunlsp  33858  irngnzply1lem  33874  irngnzply1  33875  extdgfialglem1  33876  extdgfialglem2  33877  extdgfialg  33878  ply1annig1p  33888  minplycl  33890  ply1annprmidl  33891  minplymindeg  33892  minplyann  33893  minplyirredlem  33894  minplyirred  33895  irngnminplynz  33896  minplym1p  33897  minplynzm1p  33898  minplyelirng  33899  irredminply  33900  algextdeglem1  33901  algextdeglem2  33902  algextdeglem3  33903  algextdeglem4  33904  algextdeglem5  33905  algextdeglem6  33906  algextdeglem7  33907  algextdeglem8  33908  rtelextdg2lem  33910  2sqr3minply  33964  cos9thpiminply  33972  aks6d1c1p3  42595  aks6d1c1p4  42596  aks6d1c1p5  42597  aks6d1c1p7  42598  aks6d1c1p6  42599  aks6d1c1p8  42600  aks6d1c1  42601  aks6d1c2lem3  42611  aks6d1c2lem4  42612  aks6d1c5lem0  42620  aks6d1c5lem1  42621  aks6d1c5lem3  42622  aks6d1c5  42624  aks6d1c6lem1  42655  aks6d1c6lem2  42656  aks6d1c6lem3  42657  aks6d1c6lem4  42658  aks6d1c6lem5  42662  aks5lem1  42671  aks5lem2  42672  aks5lem3a  42674  aks5lem5a  42676  prjcrv0  43083