Axiom ax-icn 7722

Description: _i is a complex number. Axiom for real and complex numbers, justified by theorem axicn 7678. (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 7629	. 2 class _i
2		cc 7625	. 2 class CC
3	1, 2	wcel 1480	1 wff _i e. CC

This axiom is referenced by:  0cn  7765  mulid1  7770  cnegexlem2  7945  cnegex  7947  0cnALT  7959  negicn  7970  ine0  8163  ixi  8352  rimul  8354  rereim  8355  apreap  8356  cru  8371  apreim  8372  mulreim  8373  apadd1  8377  apneg  8380  aprcl  8415  recextlem1  8419  recexaplem2  8420  recexap  8421  crap0  8723  cju  8726  it0e0  8948  2mulicn  8949  iap0  8950  2muliap0  8951  cnref1o  9447  irec  10399  i2  10400  i3  10401  i4  10402  iexpcyc  10404  imval  10629  imre  10630  reim  10631  crre  10636  crim  10637  remim  10639  mulreap  10643  cjreb  10645  recj  10646  reneg  10647  readd  10648  remullem  10650  imcj  10654  imneg  10655  imadd  10656  cjadd  10663  cjneg  10669  imval2  10673  rei  10678  imi  10679  cji  10681  cjreim  10682  cjreim2  10683  cjap  10685  cnrecnv  10689  rennim  10781  absi  10838  absreimsq  10846  absreim  10847  absimle  10863  climcvg1nlem  11125  sinval  11416  cosval  11417  sinf  11418  cosf  11419  tanval2ap  11427  tanval3ap  11428  resinval  11429  recosval  11430  efi4p  11431  resin4p  11432  recos4p  11433  resincl  11434  recoscl  11435  sinneg  11440  cosneg  11441  efival  11446  efmival  11447  efeul  11448  sinadd  11450  cosadd  11451  ef01bndlem  11470  sin01bnd  11471  cos01bnd  11472  absef  11483  absefib  11484  efieq1re  11485  demoivre  11486  demoivreALT  11487  cnrehmeocntop  12772  sincn  12868  coscn  12869  efhalfpi  12890  ef2kpi  12897  efper  12898  sinperlem  12899  efimpi  12910  qdencn  13232