Theorem 2cnd 9108

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

Syntax hints:   → wi 4   ∈ wcel 2175  ℂcc 7922  2c2 9086

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-11 1528  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186  ax-resscn 8016  ax-1re 8018  ax-addrcl 8021

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-in 3171  df-ss 3178  df-2 9094

This theorem is referenced by:  subhalfhalf  9271  cnm2m1cnm3  9288  xp1d2m1eqxm1d2  9289  nneo  9475  zeo2  9478  2tnp1ge0ge0  10442  flhalf  10443  fldiv4lem1div2uz2  10447  q2txmodxeq0  10527  mulbinom2  10799  binom3  10800  zesq  10801  sqoddm1div8  10836  mulsubdivbinom2ap  10854  cvg1nlemcxze  11235  resqrexlemover  11263  resqrexlemlo  11266  resqrexlemcalc1  11267  resqrexlemnm  11271  amgm2  11371  maxabslemab  11459  maxabslemlub  11460  max0addsup  11472  minabs  11489  bdtri  11493  trirecip  11754  geo2sum  11767  ege2le3  11924  efgt0  11937  tanval3ap  11967  even2n  12127  oddm1even  12128  oddp1even  12129  mulsucdiv2z  12138  ltoddhalfle  12146  m1exp1  12154  nn0enne  12155  flodddiv4  12189  flodddiv4t2lthalf  12192  bitsp1e  12205  bitsp1o  12206  bitsmod  12209  bitsinv1lem  12214  sqrt2irrlem  12425  sqrt2irr  12426  pw2dvdslemn  12429  pw2dvdseulemle  12431  oddpwdc  12438  sqrt2irraplemnn  12443  prmdiv  12499  pythagtriplem15  12543  pythagtriplem16  12544  pythagtriplem17  12545  4sqlem7  12649  4sqlem10  12652  4sqlem19  12674  2expltfac  12704  oddennn  12705  evenennn  12706  hoverb  15062  sin0pilem2  15196  perfectlem2  15414  perfect  15415  lgslem1  15419  gausslemma2dlem1a  15477  gausslemma2dlem1f1o  15479  gausslemma2dlem3  15482  gausslemma2dlem6  15486  lgseisenlem1  15489  lgseisenlem2  15490  lgseisenlem3  15491  lgseisenlem4  15492  lgsquadlem1  15496  lgsquadlem2  15497  lgsquad2lem1  15500  2lgslem1a1  15505  2lgslem1a2  15506  2lgslem1b  15508  2lgslem1c  15509  2lgslem3a1  15516  2lgslem3d1  15519  cvgcmp2nlemabs  15904  trilpolemisumle  15910  apdifflemr  15919  apdiff  15920