Theorem 2cnd 9111

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

Syntax hints:   -> wi 4   e. wcel 2176   CCcc 7925   2c2 9089

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187  ax-resscn 8019  ax-1re 8021  ax-addrcl 8024

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-in 3172  df-ss 3179  df-2 9097

This theorem is referenced by:  subhalfhalf  9274  cnm2m1cnm3  9291  xp1d2m1eqxm1d2  9292  nneo  9478  zeo2  9481  2tnp1ge0ge0  10446  flhalf  10447  fldiv4lem1div2uz2  10451  q2txmodxeq0  10531  mulbinom2  10803  binom3  10804  zesq  10805  sqoddm1div8  10840  mulsubdivbinom2ap  10858  cvg1nlemcxze  11326  resqrexlemover  11354  resqrexlemlo  11357  resqrexlemcalc1  11358  resqrexlemnm  11362  amgm2  11462  maxabslemab  11550  maxabslemlub  11551  max0addsup  11563  minabs  11580  bdtri  11584  trirecip  11845  geo2sum  11858  ege2le3  12015  efgt0  12028  tanval3ap  12058  even2n  12218  oddm1even  12219  oddp1even  12220  mulsucdiv2z  12229  ltoddhalfle  12237  m1exp1  12245  nn0enne  12246  flodddiv4  12280  flodddiv4t2lthalf  12283  bitsp1e  12296  bitsp1o  12297  bitsmod  12300  bitsinv1lem  12305  sqrt2irrlem  12516  sqrt2irr  12517  pw2dvdslemn  12520  pw2dvdseulemle  12522  oddpwdc  12529  sqrt2irraplemnn  12534  prmdiv  12590  pythagtriplem15  12634  pythagtriplem16  12635  pythagtriplem17  12636  4sqlem7  12740  4sqlem10  12743  4sqlem19  12765  2expltfac  12795  oddennn  12796  evenennn  12797  hoverb  15153  sin0pilem2  15287  perfectlem2  15505  perfect  15506  lgslem1  15510  gausslemma2dlem1a  15568  gausslemma2dlem1f1o  15570  gausslemma2dlem3  15573  gausslemma2dlem6  15577  lgseisenlem1  15580  lgseisenlem2  15581  lgseisenlem3  15582  lgseisenlem4  15583  lgsquadlem1  15587  lgsquadlem2  15588  lgsquad2lem1  15591  2lgslem1a1  15596  2lgslem1a2  15597  2lgslem1b  15599  2lgslem1c  15600  2lgslem3a1  15607  2lgslem3d1  15610  cvgcmp2nlemabs  16008  trilpolemisumle  16014  apdifflemr  16023  apdiff  16024