Metamath Proof Explorer

Theorem cnring

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

Ref Expression
Assertion cnring 
|- CCfld e. Ring

Proof

Step Hyp Ref Expression
1 cncrng 
 |-  CCfld e. CRing
2 crngring 
 |-  ( CCfld e. CRing -> CCfld e. Ring )
3 1 2 ax-mp 
 |-  CCfld e. Ring