Theorem 2cnd 9082

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

Syntax hints:   → wi 4   ∈ wcel 2167  ℂcc 7896  2c2 9060

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-resscn 7990  ax-1re 7992  ax-addrcl 7995

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170  df-2 9068

This theorem is referenced by:  subhalfhalf  9245  cnm2m1cnm3  9262  xp1d2m1eqxm1d2  9263  nneo  9448  zeo2  9451  2tnp1ge0ge0  10410  flhalf  10411  fldiv4lem1div2uz2  10415  q2txmodxeq0  10495  mulbinom2  10767  binom3  10768  zesq  10769  sqoddm1div8  10804  mulsubdivbinom2ap  10822  cvg1nlemcxze  11166  resqrexlemover  11194  resqrexlemlo  11197  resqrexlemcalc1  11198  resqrexlemnm  11202  amgm2  11302  maxabslemab  11390  maxabslemlub  11391  max0addsup  11403  minabs  11420  bdtri  11424  trirecip  11685  geo2sum  11698  ege2le3  11855  efgt0  11868  tanval3ap  11898  even2n  12058  oddm1even  12059  oddp1even  12060  mulsucdiv2z  12069  ltoddhalfle  12077  m1exp1  12085  nn0enne  12086  flodddiv4  12120  flodddiv4t2lthalf  12123  bitsp1e  12136  bitsp1o  12137  bitsmod  12140  bitsinv1lem  12145  sqrt2irrlem  12356  sqrt2irr  12357  pw2dvdslemn  12360  pw2dvdseulemle  12362  oddpwdc  12369  sqrt2irraplemnn  12374  prmdiv  12430  pythagtriplem15  12474  pythagtriplem16  12475  pythagtriplem17  12476  4sqlem7  12580  4sqlem10  12583  4sqlem19  12605  2expltfac  12635  oddennn  12636  evenennn  12637  hoverb  14992  sin0pilem2  15126  perfectlem2  15344  perfect  15345  lgslem1  15349  gausslemma2dlem1a  15407  gausslemma2dlem1f1o  15409  gausslemma2dlem3  15412  gausslemma2dlem6  15416  lgseisenlem1  15419  lgseisenlem2  15420  lgseisenlem3  15421  lgseisenlem4  15422  lgsquadlem1  15426  lgsquadlem2  15427  lgsquad2lem1  15430  2lgslem1a1  15435  2lgslem1a2  15436  2lgslem1b  15438  2lgslem1c  15439  2lgslem3a1  15446  2lgslem3d1  15449  cvgcmp2nlemabs  15789  trilpolemisumle  15795  apdifflemr  15804  apdiff  15805