Theorem 2cnd 9386

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 9384	. 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 8183   2c2 9364

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 8277  ax-1re 8279  ax-addrcl 8282

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 9372

This theorem is used by:  subhalfhalf  9551  cnm2m1cnm3  9568  xp1d2m1eqxm1d2  9569  nneo  9760  zeo2  9763  2tnp1ge0ge0  10757  flhalf  10758  fldiv4lem1div2uz2  10762  q2txmodxeq0  10842  mulbinom2  11114  binom3  11115  zesq  11117  sqoddm1div8  11152  mulsubdivbinom2ap  11171  sq01  11682  cvg1nlemcxze  11770  resqrexlemover  11798  resqrexlemlo  11801  resqrexlemcalc1  11802  resqrexlemnm  11806  amgm2  11907  maxabslemab  11995  maxabslemlub  11996  max0addsup  12008  minabs  12026  bdtri  12031  trirecip  12293  geo2sum  12306  ege2le3  12463  efgt0  12476  tanval3ap  12506  even2n  12666  oddm1even  12667  oddp1even  12668  mulsucdiv2z  12677  ltoddhalfle  12685  m1exp1  12693  nn0enne  12694  flodddiv4  12728  flodddiv4t2lthalf  12731  bitsp1e  12744  bitsp1o  12745  bitsmod  12748  bitsinv1lem  12753  sqrt2irrlem  12965  sqrt2irr  12966  sqrt2irraplemnn  12984  prmdiv  13042  pythagtriplem15  13086  pythagtriplem16  13087  pythagtriplem17  13088  4sqlem7  13192  4sqlem10  13195  4sqlem19  13217  2expltfac  13248  oddennn  13341  evenennn  13342  hoverb  15874  sin0pilem2  16009  log2tlbndlog2  16220  chtqub  16296  perfectlem2  16300  perfect  16301  bcp1ctr  16306  bclbnd  16307  bposlem1  16311  bposlem2  16312  lgslem1  16324  gausslemma2dlem1a  16382  gausslemma2dlem1f1o  16384  gausslemma2dlem3  16387  gausslemma2dlem6  16391  lgseisenlem1  16394  lgseisenlem2  16395  lgseisenlem3  16396  lgseisenlem4  16397  lgsquadlem1  16401  lgsquadlem2  16402  lgsquad2lem1  16405  2lgslem1a1  16410  2lgslem1a2  16411  2lgslem1b  16413  2lgslem1c  16414  2lgslem3a1  16421  2lgslem3d1  16424  clwwlkext2edg  16868  clwwlknonex2lem1  16883  clwwlknonex2lem2  16884  cvgcmp2nlemabs  17287  trilpolemisumle  17294  apdifflemr  17303  apdiff  17304  qdiff  17305