Theorem 2cnd 9206

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℂcc 8020  2c2 9184

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 8114  ax-1re 8116  ax-addrcl 8119

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 3204  df-ss 3211  df-2 9192

This theorem is referenced by:  subhalfhalf  9369  cnm2m1cnm3  9386  xp1d2m1eqxm1d2  9387  nneo  9573  zeo2  9576  2tnp1ge0ge0  10551  flhalf  10552  fldiv4lem1div2uz2  10556  q2txmodxeq0  10636  mulbinom2  10908  binom3  10909  zesq  10910  sqoddm1div8  10945  mulsubdivbinom2ap  10963  cvg1nlemcxze  11533  resqrexlemover  11561  resqrexlemlo  11564  resqrexlemcalc1  11565  resqrexlemnm  11569  amgm2  11669  maxabslemab  11757  maxabslemlub  11758  max0addsup  11770  minabs  11787  bdtri  11791  trirecip  12052  geo2sum  12065  ege2le3  12222  efgt0  12235  tanval3ap  12265  even2n  12425  oddm1even  12426  oddp1even  12427  mulsucdiv2z  12436  ltoddhalfle  12444  m1exp1  12452  nn0enne  12453  flodddiv4  12487  flodddiv4t2lthalf  12490  bitsp1e  12503  bitsp1o  12504  bitsmod  12507  bitsinv1lem  12512  sqrt2irrlem  12723  sqrt2irr  12724  pw2dvdslemn  12727  pw2dvdseulemle  12729  oddpwdc  12736  sqrt2irraplemnn  12741  prmdiv  12797  pythagtriplem15  12841  pythagtriplem16  12842  pythagtriplem17  12843  4sqlem7  12947  4sqlem10  12950  4sqlem19  12972  2expltfac  13002  oddennn  13003  evenennn  13004  hoverb  15362  sin0pilem2  15496  perfectlem2  15714  perfect  15715  lgslem1  15719  gausslemma2dlem1a  15777  gausslemma2dlem1f1o  15779  gausslemma2dlem3  15782  gausslemma2dlem6  15786  lgseisenlem1  15789  lgseisenlem2  15790  lgseisenlem3  15791  lgseisenlem4  15792  lgsquadlem1  15796  lgsquadlem2  15797  lgsquad2lem1  15800  2lgslem1a1  15805  2lgslem1a2  15806  2lgslem1b  15808  2lgslem1c  15809  2lgslem3a1  15816  2lgslem3d1  15819  clwwlkext2edg  16217  clwwlknonex2lem1  16232  clwwlknonex2lem2  16233  cvgcmp2nlemabs  16572  trilpolemisumle  16578  apdifflemr  16587  apdiff  16588