Theorem 2cnd 9386

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  ℂcc 8183  2c2 9364

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-resscn 8277  ax-1re 8279  ax-addrcl 8282

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233  df-2 9372

This theorem is used by:  subhalfhalf  9551  cnm2m1cnm3  9568  xp1d2m1eqxm1d2  9569  nneo  9759  zeo2  9762  2tnp1ge0ge0  10756  flhalf  10757  fldiv4lem1div2uz2  10761  q2txmodxeq0  10841  mulbinom2  11113  binom3  11114  zesq  11116  sqoddm1div8  11151  mulsubdivbinom2ap  11170  sq01  11681  cvg1nlemcxze  11769  resqrexlemover  11797  resqrexlemlo  11800  resqrexlemcalc1  11801  resqrexlemnm  11805  amgm2  11906  maxabslemab  11994  maxabslemlub  11995  max0addsup  12007  minabs  12025  bdtri  12030  trirecip  12292  geo2sum  12305  ege2le3  12462  efgt0  12475  tanval3ap  12505  even2n  12665  oddm1even  12666  oddp1even  12667  mulsucdiv2z  12676  ltoddhalfle  12684  m1exp1  12692  nn0enne  12693  flodddiv4  12727  flodddiv4t2lthalf  12730  bitsp1e  12743  bitsp1o  12744  bitsmod  12747  bitsinv1lem  12752  sqrt2irrlem  12964  sqrt2irr  12965  sqrt2irraplemnn  12983  prmdiv  13041  pythagtriplem15  13085  pythagtriplem16  13086  pythagtriplem17  13087  4sqlem7  13191  4sqlem10  13194  4sqlem19  13216  2expltfac  13247  oddennn  13340  evenennn  13341  hoverb  15891  sin0pilem2  16026  log2tlbndlog2  16237  chtqub  16313  perfectlem2  16317  perfect  16318  bcp1ctr  16323  bclbnd  16324  bposlem1  16328  bposlem2  16329  lgslem1  16341  gausslemma2dlem1a  16399  gausslemma2dlem1f1o  16401  gausslemma2dlem3  16404  gausslemma2dlem6  16408  lgseisenlem1  16411  lgseisenlem2  16412  lgseisenlem3  16413  lgseisenlem4  16414  lgsquadlem1  16418  lgsquadlem2  16419  lgsquad2lem1  16422  2lgslem1a1  16427  2lgslem1a2  16428  2lgslem1b  16430  2lgslem1c  16431  2lgslem3a1  16438  2lgslem3d1  16441  clwwlkext2edg  16885  clwwlknonex2lem1  16900  clwwlknonex2lem2  16901  cvgcmp2nlemabs  17304  trilpolemisumle  17311  apdifflemr  17320  apdiff  17321  qdiff  17322