Theorem 2cnd 8817

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

Syntax hints:   -> wi 4   e. wcel 1481   CCcc 7642   2c2 8795

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 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-11 1485  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-resscn 7736  ax-1re 7738  ax-addrcl 7741

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-in 3082  df-ss 3089  df-2 8803

This theorem is referenced by:  cnm2m1cnm3  8995  xp1d2m1eqxm1d2  8996  nneo  9178  zeo2  9181  2tnp1ge0ge0  10105  flhalf  10106  q2txmodxeq0  10188  mulbinom2  10439  binom3  10440  zesq  10441  sqoddm1div8  10475  cvg1nlemcxze  10786  resqrexlemover  10814  resqrexlemlo  10817  resqrexlemcalc1  10818  resqrexlemnm  10822  amgm2  10922  maxabslemab  11010  maxabslemlub  11011  max0addsup  11023  minabs  11039  bdtri  11043  trirecip  11302  geo2sum  11315  ege2le3  11414  efgt0  11427  tanval3ap  11457  even2n  11607  oddm1even  11608  oddp1even  11609  mulsucdiv2z  11618  ltoddhalfle  11626  m1exp1  11634  nn0enne  11635  flodddiv4  11667  flodddiv4t2lthalf  11670  sqrt2irrlem  11875  sqrt2irr  11876  pw2dvdslemn  11879  pw2dvdseulemle  11881  oddpwdc  11888  sqrt2irraplemnn  11893  oddennn  11941  evenennn  11942  sin0pilem2  12911  cvgcmp2nlemabs  13402  trilpolemisumle  13406  apdifflemr  13415  apdiff  13416