Theorem 2cnd 9194

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

Syntax hints:   -> wi 4   e. wcel 2200   CCcc 8008   2c2 9172

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-resscn 8102  ax-1re 8104  ax-addrcl 8107

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210  df-2 9180

This theorem is referenced by:  subhalfhalf  9357  cnm2m1cnm3  9374  xp1d2m1eqxm1d2  9375  nneo  9561  zeo2  9564  2tnp1ge0ge0  10533  flhalf  10534  fldiv4lem1div2uz2  10538  q2txmodxeq0  10618  mulbinom2  10890  binom3  10891  zesq  10892  sqoddm1div8  10927  mulsubdivbinom2ap  10945  cvg1nlemcxze  11509  resqrexlemover  11537  resqrexlemlo  11540  resqrexlemcalc1  11541  resqrexlemnm  11545  amgm2  11645  maxabslemab  11733  maxabslemlub  11734  max0addsup  11746  minabs  11763  bdtri  11767  trirecip  12028  geo2sum  12041  ege2le3  12198  efgt0  12211  tanval3ap  12241  even2n  12401  oddm1even  12402  oddp1even  12403  mulsucdiv2z  12412  ltoddhalfle  12420  m1exp1  12428  nn0enne  12429  flodddiv4  12463  flodddiv4t2lthalf  12466  bitsp1e  12479  bitsp1o  12480  bitsmod  12483  bitsinv1lem  12488  sqrt2irrlem  12699  sqrt2irr  12700  pw2dvdslemn  12703  pw2dvdseulemle  12705  oddpwdc  12712  sqrt2irraplemnn  12717  prmdiv  12773  pythagtriplem15  12817  pythagtriplem16  12818  pythagtriplem17  12819  4sqlem7  12923  4sqlem10  12926  4sqlem19  12948  2expltfac  12978  oddennn  12979  evenennn  12980  hoverb  15338  sin0pilem2  15472  perfectlem2  15690  perfect  15691  lgslem1  15695  gausslemma2dlem1a  15753  gausslemma2dlem1f1o  15755  gausslemma2dlem3  15758  gausslemma2dlem6  15762  lgseisenlem1  15765  lgseisenlem2  15766  lgseisenlem3  15767  lgseisenlem4  15768  lgsquadlem1  15772  lgsquadlem2  15773  lgsquad2lem1  15776  2lgslem1a1  15781  2lgslem1a2  15782  2lgslem1b  15784  2lgslem1c  15785  2lgslem3a1  15792  2lgslem3d1  15795  clwwlkext2edg  16164  cvgcmp2nlemabs  16488  trilpolemisumle  16494  apdifflemr  16503  apdiff  16504