Theorem 2cnd 8992

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

Syntax hints:   -> wi 4   e. wcel 2148   CCcc 7809   2c2 8970

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 7903  ax-1re 7905  ax-addrcl 7908

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 3136  df-ss 3143  df-2 8978

This theorem is referenced by:  cnm2m1cnm3  9170  xp1d2m1eqxm1d2  9171  nneo  9356  zeo2  9359  2tnp1ge0ge0  10301  flhalf  10302  q2txmodxeq0  10384  mulbinom2  10637  binom3  10638  zesq  10639  sqoddm1div8  10674  mulsubdivbinom2ap  10691  cvg1nlemcxze  10991  resqrexlemover  11019  resqrexlemlo  11022  resqrexlemcalc1  11023  resqrexlemnm  11027  amgm2  11127  maxabslemab  11215  maxabslemlub  11216  max0addsup  11228  minabs  11244  bdtri  11248  trirecip  11509  geo2sum  11522  ege2le3  11679  efgt0  11692  tanval3ap  11722  even2n  11879  oddm1even  11880  oddp1even  11881  mulsucdiv2z  11890  ltoddhalfle  11898  m1exp1  11906  nn0enne  11907  flodddiv4  11939  flodddiv4t2lthalf  11942  sqrt2irrlem  12161  sqrt2irr  12162  pw2dvdslemn  12165  pw2dvdseulemle  12167  oddpwdc  12174  sqrt2irraplemnn  12179  prmdiv  12235  pythagtriplem15  12278  pythagtriplem16  12279  pythagtriplem17  12280  4sqlem7  12382  4sqlem10  12385  oddennn  12393  evenennn  12394  sin0pilem2  14206  lgslem1  14404  lgseisenlem1  14453  lgseisenlem2  14454  cvgcmp2nlemabs  14783  trilpolemisumle  14789  apdifflemr  14798  apdiff  14799