Theorem 2cnd 9144

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

Syntax hints:   -> wi 4   e. wcel 2178   CCcc 7958   2c2 9122

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189  ax-resscn 8052  ax-1re 8054  ax-addrcl 8057

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-in 3180  df-ss 3187  df-2 9130

This theorem is referenced by:  subhalfhalf  9307  cnm2m1cnm3  9324  xp1d2m1eqxm1d2  9325  nneo  9511  zeo2  9514  2tnp1ge0ge0  10481  flhalf  10482  fldiv4lem1div2uz2  10486  q2txmodxeq0  10566  mulbinom2  10838  binom3  10839  zesq  10840  sqoddm1div8  10875  mulsubdivbinom2ap  10893  cvg1nlemcxze  11408  resqrexlemover  11436  resqrexlemlo  11439  resqrexlemcalc1  11440  resqrexlemnm  11444  amgm2  11544  maxabslemab  11632  maxabslemlub  11633  max0addsup  11645  minabs  11662  bdtri  11666  trirecip  11927  geo2sum  11940  ege2le3  12097  efgt0  12110  tanval3ap  12140  even2n  12300  oddm1even  12301  oddp1even  12302  mulsucdiv2z  12311  ltoddhalfle  12319  m1exp1  12327  nn0enne  12328  flodddiv4  12362  flodddiv4t2lthalf  12365  bitsp1e  12378  bitsp1o  12379  bitsmod  12382  bitsinv1lem  12387  sqrt2irrlem  12598  sqrt2irr  12599  pw2dvdslemn  12602  pw2dvdseulemle  12604  oddpwdc  12611  sqrt2irraplemnn  12616  prmdiv  12672  pythagtriplem15  12716  pythagtriplem16  12717  pythagtriplem17  12718  4sqlem7  12822  4sqlem10  12825  4sqlem19  12847  2expltfac  12877  oddennn  12878  evenennn  12879  hoverb  15235  sin0pilem2  15369  perfectlem2  15587  perfect  15588  lgslem1  15592  gausslemma2dlem1a  15650  gausslemma2dlem1f1o  15652  gausslemma2dlem3  15655  gausslemma2dlem6  15659  lgseisenlem1  15662  lgseisenlem2  15663  lgseisenlem3  15664  lgseisenlem4  15665  lgsquadlem1  15669  lgsquadlem2  15670  lgsquad2lem1  15673  2lgslem1a1  15678  2lgslem1a2  15679  2lgslem1b  15681  2lgslem1c  15682  2lgslem3a1  15689  2lgslem3d1  15692  cvgcmp2nlemabs  16173  trilpolemisumle  16179  apdifflemr  16188  apdiff  16189