Theorem cnring

Description: The complex numbers form a ring. (Contributed by Stefan O'Rear, 27-Nov-2014)

	Ref	Expression
Assertion	cnring	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$$

Proof

Step	Hyp	Ref	Expression
1		cncrng	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{CRing}$$
2		crngring	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{CRing}\to {ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$$
3	1 2	ax-mp	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$$