Axiom ax-icn 7203

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

This axiom is referenced by:  0cn  7243  mulid1  7248  cnegexlem2  7421  cnegex  7423  0cnALT  7435  negicn  7446  ine0  7635  ixi  7820  rimul  7822  rereim  7823  apreap  7824  cru  7839  apreim  7840  mulreim  7841  apadd1  7845  apneg  7848  recextlem1  7878  recexaplem2  7879  recexap  7880  crap0  8172  cju  8175  it0e0  8389  2mulicn  8390  iap0  8391  2muliap0  8392  cnref1o  8884  irec  9741  i2  9742  i3  9743  i4  9744  iexpcyc  9746  imval  9956  imre  9957  reim  9958  crre  9963  crim  9964  remim  9966  mulreap  9970  cjreb  9972  recj  9973  reneg  9974  readd  9975  remullem  9977  imcj  9981  imneg  9982  imadd  9983  cjadd  9990  cjneg  9996  imval2  10000  rei  10005  imi  10006  cji  10008  cjreim  10009  cjreim2  10010  cjap  10012  cnrecnv  10016  rennim  10107  absi  10164  absreimsq  10172  absreim  10173  absimle  10189  climcvg1nlem  10405  qdencn  11070