Axiom ax-icn 7590

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

This axiom is referenced by:  0cn  7630  mulid1  7635  cnegexlem2  7809  cnegex  7811  0cnALT  7823  negicn  7834  ine0  8023  ixi  8211  rimul  8213  rereim  8214  apreap  8215  cru  8230  apreim  8231  mulreim  8232  apadd1  8236  apneg  8239  recextlem1  8273  recexaplem2  8274  recexap  8275  crap0  8574  cju  8577  it0e0  8793  2mulicn  8794  iap0  8795  2muliap0  8796  cnref1o  9290  irec  10233  i2  10234  i3  10235  i4  10236  iexpcyc  10238  imval  10463  imre  10464  reim  10465  crre  10470  crim  10471  remim  10473  mulreap  10477  cjreb  10479  recj  10480  reneg  10481  readd  10482  remullem  10484  imcj  10488  imneg  10489  imadd  10490  cjadd  10497  cjneg  10503  imval2  10507  rei  10512  imi  10513  cji  10515  cjreim  10516  cjreim2  10517  cjap  10519  cnrecnv  10523  rennim  10614  absi  10671  absreimsq  10679  absreim  10680  absimle  10696  climcvg1nlem  10957  sinval  11207  cosval  11208  sinf  11209  cosf  11210  tanval2ap  11218  tanval3ap  11219  resinval  11220  recosval  11221  efi4p  11222  resin4p  11223  recos4p  11224  resincl  11225  recoscl  11226  sinneg  11231  cosneg  11232  efival  11237  efmival  11238  efeul  11239  sinadd  11241  cosadd  11242  ef01bndlem  11261  sin01bnd  11262  cos01bnd  11263  absef  11273  absefib  11274  efieq1re  11275  demoivre  11276  demoivreALT  11277  qdencn  12806