Theorem 2cnd 9204

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 9202	. 2 |- 2 e. CC
2	1	a1i 9	1 |- ( ph -> 2 e. CC )

Syntax hints:   -> wi 4   e. wcel 2200   CCcc 8018   2c2 9182

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-resscn 8112  ax-1re 8114  ax-addrcl 8117

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3204  df-ss 3211  df-2 9190

This theorem is referenced by:  subhalfhalf  9367  cnm2m1cnm3  9384  xp1d2m1eqxm1d2  9385  nneo  9571  zeo2  9574  2tnp1ge0ge0  10549  flhalf  10550  fldiv4lem1div2uz2  10554  q2txmodxeq0  10634  mulbinom2  10906  binom3  10907  zesq  10908  sqoddm1div8  10943  mulsubdivbinom2ap  10961  cvg1nlemcxze  11530  resqrexlemover  11558  resqrexlemlo  11561  resqrexlemcalc1  11562  resqrexlemnm  11566  amgm2  11666  maxabslemab  11754  maxabslemlub  11755  max0addsup  11767  minabs  11784  bdtri  11788  trirecip  12049  geo2sum  12062  ege2le3  12219  efgt0  12232  tanval3ap  12262  even2n  12422  oddm1even  12423  oddp1even  12424  mulsucdiv2z  12433  ltoddhalfle  12441  m1exp1  12449  nn0enne  12450  flodddiv4  12484  flodddiv4t2lthalf  12487  bitsp1e  12500  bitsp1o  12501  bitsmod  12504  bitsinv1lem  12509  sqrt2irrlem  12720  sqrt2irr  12721  pw2dvdslemn  12724  pw2dvdseulemle  12726  oddpwdc  12733  sqrt2irraplemnn  12738  prmdiv  12794  pythagtriplem15  12838  pythagtriplem16  12839  pythagtriplem17  12840  4sqlem7  12944  4sqlem10  12947  4sqlem19  12969  2expltfac  12999  oddennn  13000  evenennn  13001  hoverb  15359  sin0pilem2  15493  perfectlem2  15711  perfect  15712  lgslem1  15716  gausslemma2dlem1a  15774  gausslemma2dlem1f1o  15776  gausslemma2dlem3  15779  gausslemma2dlem6  15783  lgseisenlem1  15786  lgseisenlem2  15787  lgseisenlem3  15788  lgseisenlem4  15789  lgsquadlem1  15793  lgsquadlem2  15794  lgsquad2lem1  15797  2lgslem1a1  15802  2lgslem1a2  15803  2lgslem1b  15805  2lgslem1c  15806  2lgslem3a1  15813  2lgslem3d1  15816  clwwlkext2edg  16207  clwwlknonex2lem1  16222  clwwlknonex2lem2  16223  cvgcmp2nlemabs  16546  trilpolemisumle  16552  apdifflemr  16561  apdiff  16562