Theorem 2cnd 8179

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

Syntax hints:   -> wi 4   e. wcel 1434   CCcc 7041   2c2 8156

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-11 1438  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064  ax-resscn 7130  ax-1re 7132  ax-addrcl 7135

This theorem depends on definitions:  df-bi 115  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-in 2980  df-ss 2987  df-2 8165

This theorem is referenced by:  cnm2m1cnm3  8349  xp1d2m1eqxm1d2  8350  nneo  8531  zeo2  8534  2tnp1ge0ge0  9383  flhalf  9384  q2txmodxeq0  9466  mulbinom2  9686  binom3  9687  zesq  9688  sqoddm1div8  9722  cvg1nlemcxze  10006  resqrexlemover  10034  resqrexlemlo  10037  resqrexlemcalc1  10038  resqrexlemnm  10042  amgm2  10142  maxabslemab  10230  maxabslemlub  10231  max0addsup  10243  even2n  10418  oddm1even  10419  oddp1even  10420  mulsucdiv2z  10429  ltoddhalfle  10437  m1exp1  10445  nn0enne  10446  flodddiv4  10478  flodddiv4t2lthalf  10481  sqrt2irrlem  10684  sqrt2irr  10685  pw2dvdslemn  10687  pw2dvdseulemle  10689  oddpwdc  10696  sqrt2irraplemnn  10701  oddennn  10730  evenennn  10731