Metamath Proof Explorer


Axiom ax-icn

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

Ref Expression
Assertion ax-icn
|- _i e. CC

Detailed syntax breakdown

Step Hyp Ref Expression
0 ci
 |-  _i
1 cc
 |-  CC
2 0 1 wcel
 |-  _i e. CC