Axiom ax-icn 7967

Description: _i is a complex number. Axiom for real and complex numbers, justified by Theorem axicn 7923. (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 7874	. 2 class _i
2		cc 7870	. 2 class CC
3	1, 2	wcel 2164	1 wff _i e. CC

This axiom is referenced by:  0cn  8011  mulrid  8016  cnegexlem2  8195  cnegex  8197  0cnALT  8209  negicn  8220  ine0  8413  ixi  8602  rimul  8604  rereim  8605  apreap  8606  cru  8621  apreim  8622  mulreim  8623  apadd1  8627  apneg  8630  aprcl  8665  aptap  8669  recextlem1  8670  recexaplem2  8671  recexap  8672  crap0  8977  cju  8980  it0e0  9203  2mulicn  9204  iap0  9205  2muliap0  9206  cnref1o  9716  irec  10710  i2  10711  i3  10712  i4  10713  iexpcyc  10715  imval  10994  imre  10995  reim  10996  crre  11001  crim  11002  remim  11004  mulreap  11008  cjreb  11010  recj  11011  reneg  11012  readd  11013  remullem  11015  imcj  11019  imneg  11020  imadd  11021  cjadd  11028  cjneg  11034  imval2  11038  rei  11043  imi  11044  cji  11046  cjreim  11047  cjreim2  11048  cjap  11050  cnrecnv  11054  rennim  11146  absi  11203  absreimsq  11211  absreim  11212  absimle  11228  climcvg1nlem  11492  sinval  11845  cosval  11846  sinf  11847  cosf  11848  tanval2ap  11856  tanval3ap  11857  resinval  11858  recosval  11859  efi4p  11860  resin4p  11861  recos4p  11862  resincl  11863  recoscl  11864  sinneg  11869  cosneg  11870  efival  11875  efmival  11876  efeul  11877  sinadd  11879  cosadd  11880  ef01bndlem  11899  sin01bnd  11900  cos01bnd  11901  absef  11913  absefib  11914  efieq1re  11915  demoivre  11916  demoivreALT  11917  igz  12512  4sqlem17  12545  cnrehmeocntop  14764  sincn  14904  coscn  14905  efhalfpi  14934  ef2kpi  14941  efper  14942  sinperlem  14943  efimpi  14954  2sqlem2  15202  qdencn  15517