Description: _i is a complex number. Axiom 3 of 22 for real and complex numbers, justified by theorem axicn . (Contributed by NM, 1Mar1995)
Ref  Expression  

Assertion  axicn   _i e. CC 
Step  Hyp  Ref  Expression 

0  ci   _i 

1  cc   CC 

2  0 1  wcel   _i e. CC 