Axiom ax-icn 7071

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

This axiom is referenced by:  0cn  7111  mulid1  7116  cnegexlem2  7284  cnegex  7286  0cnALT  7298  negicn  7309  ine0  7498  ixi  7683  rimul  7685  rereim  7686  apreap  7687  cru  7702  apreim  7703  mulreim  7704  apadd1  7708  apneg  7711  recextlem1  7741  recexaplem2  7742  recexap  7743  crap0  8035  cju  8038  it0e0  8252  2mulicn  8253  iap0  8254  2muliap0  8255  cnref1o  8733  irec  9574  i2  9575  i3  9576  i4  9577  iexpcyc  9579  imval  9737  imre  9738  reim  9739  crre  9744  crim  9745  remim  9747  mulreap  9751  cjreb  9753  recj  9754  reneg  9755  readd  9756  remullem  9758  imcj  9762  imneg  9763  imadd  9764  cjadd  9771  cjneg  9777  imval2  9781  rei  9786  imi  9787  cji  9789  cjreim  9790  cjreim2  9791  cjap  9793  cnrecnv  9797  rennim  9888  absi  9945  absreimsq  9953  absreim  9954  absimle  9970  climcvg1nlem  10186  qdencn  10785