Theorem 2cnd 8926

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

Syntax hints:   -> wi 4   e. wcel 2136   CCcc 7747   2c2 8904

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 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-11 1494  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147  ax-resscn 7841  ax-1re 7843  ax-addrcl 7846

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-in 3121  df-ss 3128  df-2 8912

This theorem is referenced by:  cnm2m1cnm3  9104  xp1d2m1eqxm1d2  9105  nneo  9290  zeo2  9293  2tnp1ge0ge0  10232  flhalf  10233  q2txmodxeq0  10315  mulbinom2  10567  binom3  10568  zesq  10569  sqoddm1div8  10604  cvg1nlemcxze  10920  resqrexlemover  10948  resqrexlemlo  10951  resqrexlemcalc1  10952  resqrexlemnm  10956  amgm2  11056  maxabslemab  11144  maxabslemlub  11145  max0addsup  11157  minabs  11173  bdtri  11177  trirecip  11438  geo2sum  11451  ege2le3  11608  efgt0  11621  tanval3ap  11651  even2n  11807  oddm1even  11808  oddp1even  11809  mulsucdiv2z  11818  ltoddhalfle  11826  m1exp1  11834  nn0enne  11835  flodddiv4  11867  flodddiv4t2lthalf  11870  sqrt2irrlem  12089  sqrt2irr  12090  pw2dvdslemn  12093  pw2dvdseulemle  12095  oddpwdc  12102  sqrt2irraplemnn  12107  prmdiv  12163  pythagtriplem15  12206  pythagtriplem16  12207  pythagtriplem17  12208  4sqlem7  12310  4sqlem10  12313  oddennn  12321  evenennn  12322  sin0pilem2  13303  lgslem1  13501  cvgcmp2nlemabs  13871  trilpolemisumle  13877  apdifflemr  13886  apdiff  13887