Theorem 2cnd 9080

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

Syntax hints:   -> wi 4   e. wcel 2167   CCcc 7894   2c2 9058

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 7988  ax-1re 7990  ax-addrcl 7993

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 9066

This theorem is referenced by:  subhalfhalf  9243  cnm2m1cnm3  9260  xp1d2m1eqxm1d2  9261  nneo  9446  zeo2  9449  2tnp1ge0ge0  10408  flhalf  10409  fldiv4lem1div2uz2  10413  q2txmodxeq0  10493  mulbinom2  10765  binom3  10766  zesq  10767  sqoddm1div8  10802  mulsubdivbinom2ap  10820  cvg1nlemcxze  11164  resqrexlemover  11192  resqrexlemlo  11195  resqrexlemcalc1  11196  resqrexlemnm  11200  amgm2  11300  maxabslemab  11388  maxabslemlub  11389  max0addsup  11401  minabs  11418  bdtri  11422  trirecip  11683  geo2sum  11696  ege2le3  11853  efgt0  11866  tanval3ap  11896  even2n  12056  oddm1even  12057  oddp1even  12058  mulsucdiv2z  12067  ltoddhalfle  12075  m1exp1  12083  nn0enne  12084  flodddiv4  12118  flodddiv4t2lthalf  12121  bitsp1e  12134  bitsp1o  12135  bitsmod  12138  bitsinv1lem  12143  sqrt2irrlem  12354  sqrt2irr  12355  pw2dvdslemn  12358  pw2dvdseulemle  12360  oddpwdc  12367  sqrt2irraplemnn  12372  prmdiv  12428  pythagtriplem15  12472  pythagtriplem16  12473  pythagtriplem17  12474  4sqlem7  12578  4sqlem10  12581  4sqlem19  12603  2expltfac  12633  oddennn  12634  evenennn  12635  hoverb  14968  sin0pilem2  15102  perfectlem2  15320  perfect  15321  lgslem1  15325  gausslemma2dlem1a  15383  gausslemma2dlem1f1o  15385  gausslemma2dlem3  15388  gausslemma2dlem6  15392  lgseisenlem1  15395  lgseisenlem2  15396  lgseisenlem3  15397  lgseisenlem4  15398  lgsquadlem1  15402  lgsquadlem2  15403  lgsquad2lem1  15406  2lgslem1a1  15411  2lgslem1a2  15412  2lgslem1b  15414  2lgslem1c  15415  2lgslem3a1  15422  2lgslem3d1  15425  cvgcmp2nlemabs  15763  trilpolemisumle  15769  apdifflemr  15778  apdiff  15779