Theorem 2cnd 9275

Description: 2 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)

Assertion

Ref	Expression
2cnd	|- ( ph -> 2 e. CC )

Proof of Theorem 2cnd

Step	Hyp	Ref	Expression
1		2cn 9273	. 2 |- 2 e. CC
2	1	a1i 9	1 |- ( ph -> 2 e. CC )

Syntax hints:   -> wi 4   e. wcel 2202   CCcc 8090   2c2 9253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213  ax-resscn 8184  ax-1re 8186  ax-addrcl 8189

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214  df-2 9261

This theorem is referenced by:  subhalfhalf  9438  cnm2m1cnm3  9455  xp1d2m1eqxm1d2  9456  nneo  9644  zeo2  9647  2tnp1ge0ge0  10624  flhalf  10625  fldiv4lem1div2uz2  10629  q2txmodxeq0  10709  mulbinom2  10981  binom3  10982  zesq  10983  sqoddm1div8  11018  mulsubdivbinom2ap  11036  cvg1nlemcxze  11622  resqrexlemover  11650  resqrexlemlo  11653  resqrexlemcalc1  11654  resqrexlemnm  11658  amgm2  11758  maxabslemab  11846  maxabslemlub  11847  max0addsup  11859  minabs  11876  bdtri  11880  trirecip  12142  geo2sum  12155  ege2le3  12312  efgt0  12325  tanval3ap  12355  even2n  12515  oddm1even  12516  oddp1even  12517  mulsucdiv2z  12526  ltoddhalfle  12534  m1exp1  12542  nn0enne  12543  flodddiv4  12577  flodddiv4t2lthalf  12580  bitsp1e  12593  bitsp1o  12594  bitsmod  12597  bitsinv1lem  12602  sqrt2irrlem  12813  sqrt2irr  12814  pw2dvdslemn  12817  pw2dvdseulemle  12819  oddpwdc  12826  sqrt2irraplemnn  12831  prmdiv  12887  pythagtriplem15  12931  pythagtriplem16  12932  pythagtriplem17  12933  4sqlem7  13037  4sqlem10  13040  4sqlem19  13062  2expltfac  13092  oddennn  13093  evenennn  13094  hoverb  15459  sin0pilem2  15593  perfectlem2  15814  perfect  15815  lgslem1  15819  gausslemma2dlem1a  15877  gausslemma2dlem1f1o  15879  gausslemma2dlem3  15882  gausslemma2dlem6  15886  lgseisenlem1  15889  lgseisenlem2  15890  lgseisenlem3  15891  lgseisenlem4  15892  lgsquadlem1  15896  lgsquadlem2  15897  lgsquad2lem1  15900  2lgslem1a1  15905  2lgslem1a2  15906  2lgslem1b  15908  2lgslem1c  15909  2lgslem3a1  15916  2lgslem3d1  15919  clwwlkext2edg  16363  clwwlknonex2lem1  16378  clwwlknonex2lem2  16379  cvgcmp2nlemabs  16764  trilpolemisumle  16770  apdifflemr  16779  apdiff  16780  qdiff  16781