Theorem 2cnd 8991

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

Syntax hints:   -> wi 4   e. wcel 2148   CCcc 7808   2c2 8969

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-resscn 7902  ax-1re 7904  ax-addrcl 7907

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3135  df-ss 3142  df-2 8977

This theorem is referenced by:  cnm2m1cnm3  9169  xp1d2m1eqxm1d2  9170  nneo  9355  zeo2  9358  2tnp1ge0ge0  10300  flhalf  10301  q2txmodxeq0  10383  mulbinom2  10636  binom3  10637  zesq  10638  sqoddm1div8  10673  mulsubdivbinom2ap  10690  cvg1nlemcxze  10990  resqrexlemover  11018  resqrexlemlo  11021  resqrexlemcalc1  11022  resqrexlemnm  11026  amgm2  11126  maxabslemab  11214  maxabslemlub  11215  max0addsup  11227  minabs  11243  bdtri  11247  trirecip  11508  geo2sum  11521  ege2le3  11678  efgt0  11691  tanval3ap  11721  even2n  11878  oddm1even  11879  oddp1even  11880  mulsucdiv2z  11889  ltoddhalfle  11897  m1exp1  11905  nn0enne  11906  flodddiv4  11938  flodddiv4t2lthalf  11941  sqrt2irrlem  12160  sqrt2irr  12161  pw2dvdslemn  12164  pw2dvdseulemle  12166  oddpwdc  12173  sqrt2irraplemnn  12178  prmdiv  12234  pythagtriplem15  12277  pythagtriplem16  12278  pythagtriplem17  12279  4sqlem7  12381  4sqlem10  12384  oddennn  12392  evenennn  12393  sin0pilem2  14173  lgslem1  14371  lgseisenlem1  14420  lgseisenlem2  14421  cvgcmp2nlemabs  14750  trilpolemisumle  14756  apdifflemr  14765  apdiff  14766