Theorem 2cnd 9380

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

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

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 8272  ax-1re 8274  ax-addrcl 8277

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 9366

This theorem is used by:  subhalfhalf  9545  cnm2m1cnm3  9562  xp1d2m1eqxm1d2  9563  nneo  9754  zeo2  9757  2tnp1ge0ge0  10751  flhalf  10752  fldiv4lem1div2uz2  10756  q2txmodxeq0  10836  mulbinom2  11108  binom3  11109  zesq  11111  sqoddm1div8  11146  mulsubdivbinom2ap  11165  sq01  11676  cvg1nlemcxze  11764  resqrexlemover  11792  resqrexlemlo  11795  resqrexlemcalc1  11796  resqrexlemnm  11800  amgm2  11901  maxabslemab  11989  maxabslemlub  11990  max0addsup  12002  minabs  12020  bdtri  12025  trirecip  12287  geo2sum  12300  ege2le3  12457  efgt0  12470  tanval3ap  12500  even2n  12660  oddm1even  12661  oddp1even  12662  mulsucdiv2z  12671  ltoddhalfle  12679  m1exp1  12687  nn0enne  12688  flodddiv4  12722  flodddiv4t2lthalf  12725  bitsp1e  12738  bitsp1o  12739  bitsmod  12742  bitsinv1lem  12747  sqrt2irrlem  12959  sqrt2irr  12960  sqrt2irraplemnn  12978  prmdiv  13036  pythagtriplem15  13080  pythagtriplem16  13081  pythagtriplem17  13082  4sqlem7  13186  4sqlem10  13189  4sqlem19  13211  2expltfac  13242  oddennn  13335  evenennn  13336  hoverb  15840  sin0pilem2  15975  log2tlbndlog2  16181  chtqub  16257  perfectlem2  16261  perfect  16262  bcp1ctr  16267  bclbnd  16268  bposlem1  16272  bposlem2  16273  lgslem1  16285  gausslemma2dlem1a  16343  gausslemma2dlem1f1o  16345  gausslemma2dlem3  16348  gausslemma2dlem6  16352  lgseisenlem1  16355  lgseisenlem2  16356  lgseisenlem3  16357  lgseisenlem4  16358  lgsquadlem1  16362  lgsquadlem2  16363  lgsquad2lem1  16366  2lgslem1a1  16371  2lgslem1a2  16372  2lgslem1b  16374  2lgslem1c  16375  2lgslem3a1  16382  2lgslem3d1  16385  clwwlkext2edg  16829  clwwlknonex2lem1  16844  clwwlknonex2lem2  16845  cvgcmp2nlemabs  17247  trilpolemisumle  17254  apdifflemr  17263  apdiff  17264  qdiff  17265