Theorem 2cnd 9377

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

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   CCcc 8177   2c2 9355

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-resscn 8271  ax-1re 8273  ax-addrcl 8276

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233  df-2 9363

This theorem is used by:  subhalfhalf  9540  cnm2m1cnm3  9557  xp1d2m1eqxm1d2  9558  nneo  9749  zeo2  9752  2tnp1ge0ge0  10736  flhalf  10737  fldiv4lem1div2uz2  10741  q2txmodxeq0  10821  mulbinom2  11093  binom3  11094  zesq  11096  sqoddm1div8  11131  mulsubdivbinom2ap  11149  sq01  11660  cvg1nlemcxze  11748  resqrexlemover  11776  resqrexlemlo  11779  resqrexlemcalc1  11780  resqrexlemnm  11784  amgm2  11884  maxabslemab  11972  maxabslemlub  11973  max0addsup  11985  minabs  12002  bdtri  12006  trirecip  12268  geo2sum  12281  ege2le3  12438  efgt0  12451  tanval3ap  12481  even2n  12641  oddm1even  12642  oddp1even  12643  mulsucdiv2z  12652  ltoddhalfle  12660  m1exp1  12668  nn0enne  12669  flodddiv4  12703  flodddiv4t2lthalf  12706  bitsp1e  12719  bitsp1o  12720  bitsmod  12723  bitsinv1lem  12728  sqrt2irrlem  12939  sqrt2irr  12940  pw2dvdslemn  12943  pw2dvdseulemle  12945  oddpwdc  12952  sqrt2irraplemnn  12957  prmdiv  13013  pythagtriplem15  13057  pythagtriplem16  13058  pythagtriplem17  13059  4sqlem7  13163  4sqlem10  13166  4sqlem19  13188  2expltfac  13218  oddennn  13283  evenennn  13284  hoverb  15749  sin0pilem2  15883  log2tlbndlog2  16082  perfectlem2  16114  perfect  16115  lgslem1  16119  gausslemma2dlem1a  16177  gausslemma2dlem1f1o  16179  gausslemma2dlem3  16182  gausslemma2dlem6  16186  lgseisenlem1  16189  lgseisenlem2  16190  lgseisenlem3  16191  lgseisenlem4  16192  lgsquadlem1  16196  lgsquadlem2  16197  lgsquad2lem1  16200  2lgslem1a1  16205  2lgslem1a2  16206  2lgslem1b  16208  2lgslem1c  16209  2lgslem3a1  16216  2lgslem3d1  16219  clwwlkext2edg  16663  clwwlknonex2lem1  16678  clwwlknonex2lem2  16679  cvgcmp2nlemabs  17081  trilpolemisumle  17087  apdifflemr  17096  apdiff  17097  qdiff  17098