Theorem 2cnd 8938

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

Syntax hints:   -> wi 4   e. wcel 2141   CCcc 7759   2c2 8916

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152  ax-resscn 7853  ax-1re 7855  ax-addrcl 7858

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-in 3127  df-ss 3134  df-2 8924

This theorem is referenced by:  cnm2m1cnm3  9116  xp1d2m1eqxm1d2  9117  nneo  9302  zeo2  9305  2tnp1ge0ge0  10244  flhalf  10245  q2txmodxeq0  10327  mulbinom2  10579  binom3  10580  zesq  10581  sqoddm1div8  10616  cvg1nlemcxze  10933  resqrexlemover  10961  resqrexlemlo  10964  resqrexlemcalc1  10965  resqrexlemnm  10969  amgm2  11069  maxabslemab  11157  maxabslemlub  11158  max0addsup  11170  minabs  11186  bdtri  11190  trirecip  11451  geo2sum  11464  ege2le3  11621  efgt0  11634  tanval3ap  11664  even2n  11820  oddm1even  11821  oddp1even  11822  mulsucdiv2z  11831  ltoddhalfle  11839  m1exp1  11847  nn0enne  11848  flodddiv4  11880  flodddiv4t2lthalf  11883  sqrt2irrlem  12102  sqrt2irr  12103  pw2dvdslemn  12106  pw2dvdseulemle  12108  oddpwdc  12115  sqrt2irraplemnn  12120  prmdiv  12176  pythagtriplem15  12219  pythagtriplem16  12220  pythagtriplem17  12221  4sqlem7  12323  4sqlem10  12326  oddennn  12334  evenennn  12335  sin0pilem2  13456  lgslem1  13654  cvgcmp2nlemabs  14024  trilpolemisumle  14030  apdifflemr  14039  apdiff  14040