Axiom ax-icn 8022

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

Assertion

Ref	Expression
ax-icn	|- _i e. CC

Detailed syntax breakdown of Axiom ax-icn

Step	Hyp	Ref	Expression
1		ci 7929	. 2 class _i
2		cc 7925	. 2 class CC
3	1, 2	wcel 2176	1 wff _i e. CC

This axiom is referenced by:  0cn  8066  mulrid  8071  cnegexlem2  8250  cnegex  8252  0cnALT  8264  negicn  8275  ine0  8468  ixi  8658  rimul  8660  rereim  8661  apreap  8662  cru  8677  apreim  8678  mulreim  8679  apadd1  8683  apneg  8686  aprcl  8721  aptap  8725  recextlem1  8726  recexaplem2  8727  recexap  8728  crap0  9033  cju  9036  it0e0  9260  2mulicn  9261  iap0  9262  2muliap0  9263  cnref1o  9774  irec  10786  i2  10787  i3  10788  i4  10789  iexpcyc  10791  imval  11194  imre  11195  reim  11196  crre  11201  crim  11202  remim  11204  mulreap  11208  cjreb  11210  recj  11211  reneg  11212  readd  11213  remullem  11215  imcj  11219  imneg  11220  imadd  11221  cjadd  11228  cjneg  11234  imval2  11238  rei  11243  imi  11244  cji  11246  cjreim  11247  cjreim2  11248  cjap  11250  cnrecnv  11254  rennim  11346  absi  11403  absreimsq  11411  absreim  11412  absimle  11428  climcvg1nlem  11693  sinval  12046  cosval  12047  sinf  12048  cosf  12049  tanval2ap  12057  tanval3ap  12058  resinval  12059  recosval  12060  efi4p  12061  resin4p  12062  recos4p  12063  resincl  12064  recoscl  12065  sinneg  12070  cosneg  12071  efival  12076  efmival  12077  efeul  12078  sinadd  12080  cosadd  12081  ef01bndlem  12100  sin01bnd  12101  cos01bnd  12102  absef  12114  absefib  12115  efieq1re  12116  demoivre  12117  demoivreALT  12118  igz  12730  4sqlem17  12763  cnrehmeocntop  15115  sincn  15274  coscn  15275  efhalfpi  15304  ef2kpi  15311  efper  15312  sinperlem  15313  efimpi  15324  2sqlem2  15625  qdencn  16003