Theorem 2cnd 9216

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

Syntax hints:   → wi 4   ∈ wcel 2202  ℂcc 8030  2c2 9194

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-resscn 8124  ax-1re 8126  ax-addrcl 8129

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213  df-2 9202

This theorem is referenced by:  subhalfhalf  9379  cnm2m1cnm3  9396  xp1d2m1eqxm1d2  9397  nneo  9583  zeo2  9586  2tnp1ge0ge0  10562  flhalf  10563  fldiv4lem1div2uz2  10567  q2txmodxeq0  10647  mulbinom2  10919  binom3  10920  zesq  10921  sqoddm1div8  10956  mulsubdivbinom2ap  10974  cvg1nlemcxze  11547  resqrexlemover  11575  resqrexlemlo  11578  resqrexlemcalc1  11579  resqrexlemnm  11583  amgm2  11683  maxabslemab  11771  maxabslemlub  11772  max0addsup  11784  minabs  11801  bdtri  11805  trirecip  12067  geo2sum  12080  ege2le3  12237  efgt0  12250  tanval3ap  12280  even2n  12440  oddm1even  12441  oddp1even  12442  mulsucdiv2z  12451  ltoddhalfle  12459  m1exp1  12467  nn0enne  12468  flodddiv4  12502  flodddiv4t2lthalf  12505  bitsp1e  12518  bitsp1o  12519  bitsmod  12522  bitsinv1lem  12527  sqrt2irrlem  12738  sqrt2irr  12739  pw2dvdslemn  12742  pw2dvdseulemle  12744  oddpwdc  12751  sqrt2irraplemnn  12756  prmdiv  12812  pythagtriplem15  12856  pythagtriplem16  12857  pythagtriplem17  12858  4sqlem7  12962  4sqlem10  12965  4sqlem19  12987  2expltfac  13017  oddennn  13018  evenennn  13019  hoverb  15378  sin0pilem2  15512  perfectlem2  15730  perfect  15731  lgslem1  15735  gausslemma2dlem1a  15793  gausslemma2dlem1f1o  15795  gausslemma2dlem3  15798  gausslemma2dlem6  15802  lgseisenlem1  15805  lgseisenlem2  15806  lgseisenlem3  15807  lgseisenlem4  15808  lgsquadlem1  15812  lgsquadlem2  15813  lgsquad2lem1  15816  2lgslem1a1  15821  2lgslem1a2  15822  2lgslem1b  15824  2lgslem1c  15825  2lgslem3a1  15832  2lgslem3d1  15835  clwwlkext2edg  16279  clwwlknonex2lem1  16294  clwwlknonex2lem2  16295  cvgcmp2nlemabs  16662  trilpolemisumle  16668  apdifflemr  16677  apdiff  16678  qdiff  16679