Theorem 2cnd 9055

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

Syntax hints:   -> wi 4   e. wcel 2164   CCcc 7870   2c2 9033

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 2175  ax-resscn 7964  ax-1re 7966  ax-addrcl 7969

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3159  df-ss 3166  df-2 9041

This theorem is referenced by:  subhalfhalf  9217  cnm2m1cnm3  9234  xp1d2m1eqxm1d2  9235  nneo  9420  zeo2  9423  2tnp1ge0ge0  10370  flhalf  10371  fldiv4lem1div2uz2  10375  q2txmodxeq0  10455  mulbinom2  10727  binom3  10728  zesq  10729  sqoddm1div8  10764  mulsubdivbinom2ap  10782  cvg1nlemcxze  11126  resqrexlemover  11154  resqrexlemlo  11157  resqrexlemcalc1  11158  resqrexlemnm  11162  amgm2  11262  maxabslemab  11350  maxabslemlub  11351  max0addsup  11363  minabs  11379  bdtri  11383  trirecip  11644  geo2sum  11657  ege2le3  11814  efgt0  11827  tanval3ap  11857  even2n  12015  oddm1even  12016  oddp1even  12017  mulsucdiv2z  12026  ltoddhalfle  12034  m1exp1  12042  nn0enne  12043  flodddiv4  12075  flodddiv4t2lthalf  12078  sqrt2irrlem  12299  sqrt2irr  12300  pw2dvdslemn  12303  pw2dvdseulemle  12305  oddpwdc  12312  sqrt2irraplemnn  12317  prmdiv  12373  pythagtriplem15  12416  pythagtriplem16  12417  pythagtriplem17  12418  4sqlem7  12522  4sqlem10  12525  4sqlem19  12547  oddennn  12549  evenennn  12550  hoverb  14802  sin0pilem2  14917  lgslem1  15116  gausslemma2dlem1a  15174  gausslemma2dlem1f1o  15176  gausslemma2dlem3  15179  gausslemma2dlem6  15183  lgseisenlem1  15186  lgseisenlem2  15187  lgseisenlem3  15188  lgseisenlem4  15189  lgsquadlem1  15191  cvgcmp2nlemabs  15522  trilpolemisumle  15528  apdifflemr  15537  apdiff  15538