Theorem 2cnd 9327

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

Syntax hints:   -> wi 4   e. wcel 2205   CCcc 8141   2c2 9305

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216  ax-resscn 8235  ax-1re 8237  ax-addrcl 8240

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-in 3220  df-ss 3227  df-2 9313

This theorem is referenced by:  subhalfhalf  9490  cnm2m1cnm3  9507  xp1d2m1eqxm1d2  9508  nneo  9699  zeo2  9702  2tnp1ge0ge0  10685  flhalf  10686  fldiv4lem1div2uz2  10690  q2txmodxeq0  10770  mulbinom2  11042  binom3  11043  zesq  11045  sqoddm1div8  11080  mulsubdivbinom2ap  11098  cvg1nlemcxze  11692  resqrexlemover  11720  resqrexlemlo  11723  resqrexlemcalc1  11724  resqrexlemnm  11728  amgm2  11828  maxabslemab  11916  maxabslemlub  11917  max0addsup  11929  minabs  11946  bdtri  11950  trirecip  12212  geo2sum  12225  ege2le3  12382  efgt0  12395  tanval3ap  12425  even2n  12585  oddm1even  12586  oddp1even  12587  mulsucdiv2z  12596  ltoddhalfle  12604  m1exp1  12612  nn0enne  12613  flodddiv4  12647  flodddiv4t2lthalf  12650  bitsp1e  12663  bitsp1o  12664  bitsmod  12667  bitsinv1lem  12672  sqrt2irrlem  12883  sqrt2irr  12884  pw2dvdslemn  12887  pw2dvdseulemle  12889  oddpwdc  12896  sqrt2irraplemnn  12901  prmdiv  12957  pythagtriplem15  13001  pythagtriplem16  13002  pythagtriplem17  13003  4sqlem7  13107  4sqlem10  13110  4sqlem19  13132  2expltfac  13162  oddennn  13227  evenennn  13228  hoverb  15639  sin0pilem2  15773  perfectlem2  15994  perfect  15995  lgslem1  15999  gausslemma2dlem1a  16057  gausslemma2dlem1f1o  16059  gausslemma2dlem3  16062  gausslemma2dlem6  16066  lgseisenlem1  16069  lgseisenlem2  16070  lgseisenlem3  16071  lgseisenlem4  16072  lgsquadlem1  16076  lgsquadlem2  16077  lgsquad2lem1  16080  2lgslem1a1  16085  2lgslem1a2  16086  2lgslem1b  16088  2lgslem1c  16089  2lgslem3a1  16096  2lgslem3d1  16099  clwwlkext2edg  16543  clwwlknonex2lem1  16558  clwwlknonex2lem2  16559  cvgcmp2nlemabs  16942  trilpolemisumle  16948  apdifflemr  16957  apdiff  16958  qdiff  16959