Theorem 2cnd 9023

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

Syntax hints:   -> wi 4   e. wcel 2160   CCcc 7840   2c2 9001

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171  ax-resscn 7934  ax-1re 7936  ax-addrcl 7939

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-in 3150  df-ss 3157  df-2 9009

This theorem is referenced by:  cnm2m1cnm3  9201  xp1d2m1eqxm1d2  9202  nneo  9387  zeo2  9390  2tnp1ge0ge0  10334  flhalf  10335  q2txmodxeq0  10417  mulbinom2  10671  binom3  10672  zesq  10673  sqoddm1div8  10708  mulsubdivbinom2ap  10726  cvg1nlemcxze  11026  resqrexlemover  11054  resqrexlemlo  11057  resqrexlemcalc1  11058  resqrexlemnm  11062  amgm2  11162  maxabslemab  11250  maxabslemlub  11251  max0addsup  11263  minabs  11279  bdtri  11283  trirecip  11544  geo2sum  11557  ege2le3  11714  efgt0  11727  tanval3ap  11757  even2n  11914  oddm1even  11915  oddp1even  11916  mulsucdiv2z  11925  ltoddhalfle  11933  m1exp1  11941  nn0enne  11942  flodddiv4  11974  flodddiv4t2lthalf  11977  sqrt2irrlem  12196  sqrt2irr  12197  pw2dvdslemn  12200  pw2dvdseulemle  12202  oddpwdc  12209  sqrt2irraplemnn  12214  prmdiv  12270  pythagtriplem15  12313  pythagtriplem16  12314  pythagtriplem17  12315  4sqlem7  12419  4sqlem10  12422  4sqlem19  12444  oddennn  12446  evenennn  12447  sin0pilem2  14680  lgslem1  14879  lgseisenlem1  14928  lgseisenlem2  14929  cvgcmp2nlemabs  15259  trilpolemisumle  15265  apdifflemr  15274  apdiff  15275