Theorem 2cnd 9259

Description: 2 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)

Assertion

Ref	Expression
2cnd	⊢ (𝜑 → 2 ∈ ℂ)

Proof of Theorem 2cnd

Step	Hyp	Ref	Expression
1		2cn 9257	. 2 ⊢ 2 ∈ ℂ
2	1	a1i 9	1 ⊢ (𝜑 → 2 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2202  ℂcc 8073  2c2 9237

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213  ax-resscn 8167  ax-1re 8169  ax-addrcl 8172

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214  df-2 9245

This theorem is referenced by:  subhalfhalf  9422  cnm2m1cnm3  9439  xp1d2m1eqxm1d2  9440  nneo  9626  zeo2  9629  2tnp1ge0ge0  10605  flhalf  10606  fldiv4lem1div2uz2  10610  q2txmodxeq0  10690  mulbinom2  10962  binom3  10963  zesq  10964  sqoddm1div8  10999  mulsubdivbinom2ap  11017  cvg1nlemcxze  11603  resqrexlemover  11631  resqrexlemlo  11634  resqrexlemcalc1  11635  resqrexlemnm  11639  amgm2  11739  maxabslemab  11827  maxabslemlub  11828  max0addsup  11840  minabs  11857  bdtri  11861  trirecip  12123  geo2sum  12136  ege2le3  12293  efgt0  12306  tanval3ap  12336  even2n  12496  oddm1even  12497  oddp1even  12498  mulsucdiv2z  12507  ltoddhalfle  12515  m1exp1  12523  nn0enne  12524  flodddiv4  12558  flodddiv4t2lthalf  12561  bitsp1e  12574  bitsp1o  12575  bitsmod  12578  bitsinv1lem  12583  sqrt2irrlem  12794  sqrt2irr  12795  pw2dvdslemn  12798  pw2dvdseulemle  12800  oddpwdc  12807  sqrt2irraplemnn  12812  prmdiv  12868  pythagtriplem15  12912  pythagtriplem16  12913  pythagtriplem17  12914  4sqlem7  13018  4sqlem10  13021  4sqlem19  13043  2expltfac  13073  oddennn  13074  evenennn  13075  hoverb  15439  sin0pilem2  15573  perfectlem2  15791  perfect  15792  lgslem1  15796  gausslemma2dlem1a  15854  gausslemma2dlem1f1o  15856  gausslemma2dlem3  15859  gausslemma2dlem6  15863  lgseisenlem1  15866  lgseisenlem2  15867  lgseisenlem3  15868  lgseisenlem4  15869  lgsquadlem1  15873  lgsquadlem2  15874  lgsquad2lem1  15877  2lgslem1a1  15882  2lgslem1a2  15883  2lgslem1b  15885  2lgslem1c  15886  2lgslem3a1  15893  2lgslem3d1  15896  clwwlkext2edg  16340  clwwlknonex2lem1  16355  clwwlknonex2lem2  16356  cvgcmp2nlemabs  16741  trilpolemisumle  16747  apdifflemr  16756  apdiff  16757  qdiff  16758