Theorem 2cnd 9183

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

Syntax hints:   -> wi 4   e. wcel 2200   CCcc 7997   2c2 9161

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 8091  ax-1re 8093  ax-addrcl 8096

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 9169

This theorem is referenced by:  subhalfhalf  9346  cnm2m1cnm3  9363  xp1d2m1eqxm1d2  9364  nneo  9550  zeo2  9553  2tnp1ge0ge0  10521  flhalf  10522  fldiv4lem1div2uz2  10526  q2txmodxeq0  10606  mulbinom2  10878  binom3  10879  zesq  10880  sqoddm1div8  10915  mulsubdivbinom2ap  10933  cvg1nlemcxze  11493  resqrexlemover  11521  resqrexlemlo  11524  resqrexlemcalc1  11525  resqrexlemnm  11529  amgm2  11629  maxabslemab  11717  maxabslemlub  11718  max0addsup  11730  minabs  11747  bdtri  11751  trirecip  12012  geo2sum  12025  ege2le3  12182  efgt0  12195  tanval3ap  12225  even2n  12385  oddm1even  12386  oddp1even  12387  mulsucdiv2z  12396  ltoddhalfle  12404  m1exp1  12412  nn0enne  12413  flodddiv4  12447  flodddiv4t2lthalf  12450  bitsp1e  12463  bitsp1o  12464  bitsmod  12467  bitsinv1lem  12472  sqrt2irrlem  12683  sqrt2irr  12684  pw2dvdslemn  12687  pw2dvdseulemle  12689  oddpwdc  12696  sqrt2irraplemnn  12701  prmdiv  12757  pythagtriplem15  12801  pythagtriplem16  12802  pythagtriplem17  12803  4sqlem7  12907  4sqlem10  12910  4sqlem19  12932  2expltfac  12962  oddennn  12963  evenennn  12964  hoverb  15322  sin0pilem2  15456  perfectlem2  15674  perfect  15675  lgslem1  15679  gausslemma2dlem1a  15737  gausslemma2dlem1f1o  15739  gausslemma2dlem3  15742  gausslemma2dlem6  15746  lgseisenlem1  15749  lgseisenlem2  15750  lgseisenlem3  15751  lgseisenlem4  15752  lgsquadlem1  15756  lgsquadlem2  15757  lgsquad2lem1  15760  2lgslem1a1  15765  2lgslem1a2  15766  2lgslem1b  15768  2lgslem1c  15769  2lgslem3a1  15776  2lgslem3d1  15779  cvgcmp2nlemabs  16400  trilpolemisumle  16406  apdifflemr  16415  apdiff  16416