Theorem 2cnd 8786

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

Syntax hints:   -> wi 4   e. wcel 1480   CCcc 7611   2c2 8764

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 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119  ax-resscn 7705  ax-1re 7707  ax-addrcl 7710

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-in 3072  df-ss 3079  df-2 8772

This theorem is referenced by:  cnm2m1cnm3  8964  xp1d2m1eqxm1d2  8965  nneo  9147  zeo2  9150  2tnp1ge0ge0  10067  flhalf  10068  q2txmodxeq0  10150  mulbinom2  10401  binom3  10402  zesq  10403  sqoddm1div8  10437  cvg1nlemcxze  10747  resqrexlemover  10775  resqrexlemlo  10778  resqrexlemcalc1  10779  resqrexlemnm  10783  amgm2  10883  maxabslemab  10971  maxabslemlub  10972  max0addsup  10984  minabs  11000  bdtri  11004  trirecip  11263  geo2sum  11276  ege2le3  11366  efgt0  11379  tanval3ap  11410  even2n  11560  oddm1even  11561  oddp1even  11562  mulsucdiv2z  11571  ltoddhalfle  11579  m1exp1  11587  nn0enne  11588  flodddiv4  11620  flodddiv4t2lthalf  11623  sqrt2irrlem  11828  sqrt2irr  11829  pw2dvdslemn  11832  pw2dvdseulemle  11834  oddpwdc  11841  sqrt2irraplemnn  11846  oddennn  11894  evenennn  11895  sin0pilem2  12852  cvgcmp2nlemabs  13216  trilpolemisumle  13220