Theorem 2cnd 9063

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

Syntax hints:   -> wi 4   e. wcel 2167   CCcc 7877   2c2 9041

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-resscn 7971  ax-1re 7973  ax-addrcl 7976

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170  df-2 9049

This theorem is referenced by:  subhalfhalf  9226  cnm2m1cnm3  9243  xp1d2m1eqxm1d2  9244  nneo  9429  zeo2  9432  2tnp1ge0ge0  10391  flhalf  10392  fldiv4lem1div2uz2  10396  q2txmodxeq0  10476  mulbinom2  10748  binom3  10749  zesq  10750  sqoddm1div8  10785  mulsubdivbinom2ap  10803  cvg1nlemcxze  11147  resqrexlemover  11175  resqrexlemlo  11178  resqrexlemcalc1  11179  resqrexlemnm  11183  amgm2  11283  maxabslemab  11371  maxabslemlub  11372  max0addsup  11384  minabs  11401  bdtri  11405  trirecip  11666  geo2sum  11679  ege2le3  11836  efgt0  11849  tanval3ap  11879  even2n  12039  oddm1even  12040  oddp1even  12041  mulsucdiv2z  12050  ltoddhalfle  12058  m1exp1  12066  nn0enne  12067  flodddiv4  12101  flodddiv4t2lthalf  12104  bitsp1e  12116  bitsp1o  12117  sqrt2irrlem  12329  sqrt2irr  12330  pw2dvdslemn  12333  pw2dvdseulemle  12335  oddpwdc  12342  sqrt2irraplemnn  12347  prmdiv  12403  pythagtriplem15  12447  pythagtriplem16  12448  pythagtriplem17  12449  4sqlem7  12553  4sqlem10  12556  4sqlem19  12578  2expltfac  12608  oddennn  12609  evenennn  12610  hoverb  14884  sin0pilem2  15018  perfectlem2  15236  perfect  15237  lgslem1  15241  gausslemma2dlem1a  15299  gausslemma2dlem1f1o  15301  gausslemma2dlem3  15304  gausslemma2dlem6  15308  lgseisenlem1  15311  lgseisenlem2  15312  lgseisenlem3  15313  lgseisenlem4  15314  lgsquadlem1  15318  lgsquadlem2  15319  lgsquad2lem1  15322  2lgslem1a1  15327  2lgslem1a2  15328  2lgslem1b  15330  2lgslem1c  15331  2lgslem3a1  15338  2lgslem3d1  15341  cvgcmp2nlemabs  15676  trilpolemisumle  15682  apdifflemr  15691  apdiff  15692