Theorem 2cnd 9215

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

Syntax hints:   → wi 4   ∈ wcel 2202  ℂcc 8029  2c2 9193

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 8123  ax-1re 8125  ax-addrcl 8128

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 9201

This theorem is referenced by:  subhalfhalf  9378  cnm2m1cnm3  9395  xp1d2m1eqxm1d2  9396  nneo  9582  zeo2  9585  2tnp1ge0ge0  10560  flhalf  10561  fldiv4lem1div2uz2  10565  q2txmodxeq0  10645  mulbinom2  10917  binom3  10918  zesq  10919  sqoddm1div8  10954  mulsubdivbinom2ap  10972  cvg1nlemcxze  11542  resqrexlemover  11570  resqrexlemlo  11573  resqrexlemcalc1  11574  resqrexlemnm  11578  amgm2  11678  maxabslemab  11766  maxabslemlub  11767  max0addsup  11779  minabs  11796  bdtri  11800  trirecip  12061  geo2sum  12074  ege2le3  12231  efgt0  12244  tanval3ap  12274  even2n  12434  oddm1even  12435  oddp1even  12436  mulsucdiv2z  12445  ltoddhalfle  12453  m1exp1  12461  nn0enne  12462  flodddiv4  12496  flodddiv4t2lthalf  12499  bitsp1e  12512  bitsp1o  12513  bitsmod  12516  bitsinv1lem  12521  sqrt2irrlem  12732  sqrt2irr  12733  pw2dvdslemn  12736  pw2dvdseulemle  12738  oddpwdc  12745  sqrt2irraplemnn  12750  prmdiv  12806  pythagtriplem15  12850  pythagtriplem16  12851  pythagtriplem17  12852  4sqlem7  12956  4sqlem10  12959  4sqlem19  12981  2expltfac  13011  oddennn  13012  evenennn  13013  hoverb  15371  sin0pilem2  15505  perfectlem2  15723  perfect  15724  lgslem1  15728  gausslemma2dlem1a  15786  gausslemma2dlem1f1o  15788  gausslemma2dlem3  15791  gausslemma2dlem6  15795  lgseisenlem1  15798  lgseisenlem2  15799  lgseisenlem3  15800  lgseisenlem4  15801  lgsquadlem1  15805  lgsquadlem2  15806  lgsquad2lem1  15809  2lgslem1a1  15814  2lgslem1a2  15815  2lgslem1b  15817  2lgslem1c  15818  2lgslem3a1  15825  2lgslem3d1  15828  clwwlkext2edg  16272  clwwlknonex2lem1  16287  clwwlknonex2lem2  16288  cvgcmp2nlemabs  16636  trilpolemisumle  16642  apdifflemr  16651  apdiff  16652