Axiom ax-icn 7036

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

This axiom is referenced by:  0cn  7076  mulid1  7081  cnegexlem2  7249  cnegex  7251  0cnALT  7263  negicn  7274  ine0  7462  ixi  7647  rimul  7649  rereim  7650  apreap  7651  cru  7666  apreim  7667  mulreim  7668  apadd1  7672  apneg  7675  recextlem1  7705  recexaplem2  7706  recexap  7707  crap0  7985  cju  7988  it0e0  8202  2mulicn  8203  iap0  8204  2muliap0  8205  cnref1o  8679  irec  9517  i2  9518  i3  9519  i4  9520  iexpcyc  9522  imval  9677  imre  9678  reim  9679  crre  9684  crim  9685  remim  9687  mulreap  9691  cjreb  9693  recj  9694  reneg  9695  readd  9696  remullem  9698  imcj  9702  imneg  9703  imadd  9704  cjadd  9711  cjneg  9717  imval2  9721  rei  9726  imi  9727  cji  9729  cjreim  9730  cjreim2  9731  cjap  9733  cnrecnv  9737  rennim  9828  absi  9885  absreimsq  9893  absreim  9894  absimle  9910  climcvg1nlem  10098  qdencn  10490