Theorem 2cnd 8593

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

Syntax hints:   -> wi 4   e. wcel 1445   CCcc 7445   2c2 8571

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-11 1449  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077  ax-resscn 7534  ax-1re 7536  ax-addrcl 7539

This theorem depends on definitions:  df-bi 116  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-in 3019  df-ss 3026  df-2 8579

This theorem is referenced by:  cnm2m1cnm3  8765  xp1d2m1eqxm1d2  8766  nneo  8948  zeo2  8951  2tnp1ge0ge0  9857  flhalf  9858  q2txmodxeq0  9940  mulbinom2  10201  binom3  10202  zesq  10203  sqoddm1div8  10237  cvg1nlemcxze  10546  resqrexlemover  10574  resqrexlemlo  10577  resqrexlemcalc1  10578  resqrexlemnm  10582  amgm2  10682  maxabslemab  10770  maxabslemlub  10771  max0addsup  10783  minabs  10798  bdtri  10802  trirecip  11060  geo2sum  11073  ege2le3  11126  efgt0  11139  tanval3ap  11170  even2n  11317  oddm1even  11318  oddp1even  11319  mulsucdiv2z  11328  ltoddhalfle  11336  m1exp1  11344  nn0enne  11345  flodddiv4  11377  flodddiv4t2lthalf  11380  sqrt2irrlem  11583  sqrt2irr  11584  pw2dvdslemn  11586  pw2dvdseulemle  11588  oddpwdc  11595  sqrt2irraplemnn  11600  oddennn  11648  evenennn  11649