Theorem 2cnd 9194

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 9192	. 2 ⊢ 2 ∈ ℂ
2	1	a1i 9	1 ⊢ (𝜑 → 2 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2200  ℂcc 8008  2c2 9172

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-resscn 8102  ax-1re 8104  ax-addrcl 8107

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210  df-2 9180

This theorem is referenced by:  subhalfhalf  9357  cnm2m1cnm3  9374  xp1d2m1eqxm1d2  9375  nneo  9561  zeo2  9564  2tnp1ge0ge0  10533  flhalf  10534  fldiv4lem1div2uz2  10538  q2txmodxeq0  10618  mulbinom2  10890  binom3  10891  zesq  10892  sqoddm1div8  10927  mulsubdivbinom2ap  10945  cvg1nlemcxze  11508  resqrexlemover  11536  resqrexlemlo  11539  resqrexlemcalc1  11540  resqrexlemnm  11544  amgm2  11644  maxabslemab  11732  maxabslemlub  11733  max0addsup  11745  minabs  11762  bdtri  11766  trirecip  12027  geo2sum  12040  ege2le3  12197  efgt0  12210  tanval3ap  12240  even2n  12400  oddm1even  12401  oddp1even  12402  mulsucdiv2z  12411  ltoddhalfle  12419  m1exp1  12427  nn0enne  12428  flodddiv4  12462  flodddiv4t2lthalf  12465  bitsp1e  12478  bitsp1o  12479  bitsmod  12482  bitsinv1lem  12487  sqrt2irrlem  12698  sqrt2irr  12699  pw2dvdslemn  12702  pw2dvdseulemle  12704  oddpwdc  12711  sqrt2irraplemnn  12716  prmdiv  12772  pythagtriplem15  12816  pythagtriplem16  12817  pythagtriplem17  12818  4sqlem7  12922  4sqlem10  12925  4sqlem19  12947  2expltfac  12977  oddennn  12978  evenennn  12979  hoverb  15337  sin0pilem2  15471  perfectlem2  15689  perfect  15690  lgslem1  15694  gausslemma2dlem1a  15752  gausslemma2dlem1f1o  15754  gausslemma2dlem3  15757  gausslemma2dlem6  15761  lgseisenlem1  15764  lgseisenlem2  15765  lgseisenlem3  15766  lgseisenlem4  15767  lgsquadlem1  15771  lgsquadlem2  15772  lgsquad2lem1  15775  2lgslem1a1  15780  2lgslem1a2  15781  2lgslem1b  15783  2lgslem1c  15784  2lgslem3a1  15791  2lgslem3d1  15794  cvgcmp2nlemabs  16460  trilpolemisumle  16466  apdifflemr  16475  apdiff  16476