Theorem 2cnd 9216

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

Syntax hints:   -> wi 4   e. wcel 2202   CCcc 8030   2c2 9194

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-resscn 8124  ax-1re 8126  ax-addrcl 8129

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213  df-2 9202

This theorem is referenced by:  subhalfhalf  9379  cnm2m1cnm3  9396  xp1d2m1eqxm1d2  9397  nneo  9583  zeo2  9586  2tnp1ge0ge0  10562  flhalf  10563  fldiv4lem1div2uz2  10567  q2txmodxeq0  10647  mulbinom2  10919  binom3  10920  zesq  10921  sqoddm1div8  10956  mulsubdivbinom2ap  10974  cvg1nlemcxze  11560  resqrexlemover  11588  resqrexlemlo  11591  resqrexlemcalc1  11592  resqrexlemnm  11596  amgm2  11696  maxabslemab  11784  maxabslemlub  11785  max0addsup  11797  minabs  11814  bdtri  11818  trirecip  12080  geo2sum  12093  ege2le3  12250  efgt0  12263  tanval3ap  12293  even2n  12453  oddm1even  12454  oddp1even  12455  mulsucdiv2z  12464  ltoddhalfle  12472  m1exp1  12480  nn0enne  12481  flodddiv4  12515  flodddiv4t2lthalf  12518  bitsp1e  12531  bitsp1o  12532  bitsmod  12535  bitsinv1lem  12540  sqrt2irrlem  12751  sqrt2irr  12752  pw2dvdslemn  12755  pw2dvdseulemle  12757  oddpwdc  12764  sqrt2irraplemnn  12769  prmdiv  12825  pythagtriplem15  12869  pythagtriplem16  12870  pythagtriplem17  12871  4sqlem7  12975  4sqlem10  12978  4sqlem19  13000  2expltfac  13030  oddennn  13031  evenennn  13032  hoverb  15391  sin0pilem2  15525  perfectlem2  15743  perfect  15744  lgslem1  15748  gausslemma2dlem1a  15806  gausslemma2dlem1f1o  15808  gausslemma2dlem3  15811  gausslemma2dlem6  15815  lgseisenlem1  15818  lgseisenlem2  15819  lgseisenlem3  15820  lgseisenlem4  15821  lgsquadlem1  15825  lgsquadlem2  15826  lgsquad2lem1  15829  2lgslem1a1  15834  2lgslem1a2  15835  2lgslem1b  15837  2lgslem1c  15838  2lgslem3a1  15845  2lgslem3d1  15848  clwwlkext2edg  16292  clwwlknonex2lem1  16307  clwwlknonex2lem2  16308  cvgcmp2nlemabs  16687  trilpolemisumle  16693  apdifflemr  16702  apdiff  16703  qdiff  16704