Theorem 2cnd 8930

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

Syntax hints:   → wi 4   ∈ wcel 2136  ℂcc 7751  2c2 8908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-11 1494  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147  ax-resscn 7845  ax-1re 7847  ax-addrcl 7850

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-in 3122  df-ss 3129  df-2 8916

This theorem is referenced by:  cnm2m1cnm3  9108  xp1d2m1eqxm1d2  9109  nneo  9294  zeo2  9297  2tnp1ge0ge0  10236  flhalf  10237  q2txmodxeq0  10319  mulbinom2  10571  binom3  10572  zesq  10573  sqoddm1div8  10608  cvg1nlemcxze  10924  resqrexlemover  10952  resqrexlemlo  10955  resqrexlemcalc1  10956  resqrexlemnm  10960  amgm2  11060  maxabslemab  11148  maxabslemlub  11149  max0addsup  11161  minabs  11177  bdtri  11181  trirecip  11442  geo2sum  11455  ege2le3  11612  efgt0  11625  tanval3ap  11655  even2n  11811  oddm1even  11812  oddp1even  11813  mulsucdiv2z  11822  ltoddhalfle  11830  m1exp1  11838  nn0enne  11839  flodddiv4  11871  flodddiv4t2lthalf  11874  sqrt2irrlem  12093  sqrt2irr  12094  pw2dvdslemn  12097  pw2dvdseulemle  12099  oddpwdc  12106  sqrt2irraplemnn  12111  prmdiv  12167  pythagtriplem15  12210  pythagtriplem16  12211  pythagtriplem17  12212  4sqlem7  12314  4sqlem10  12317  oddennn  12325  evenennn  12326  sin0pilem2  13343  lgslem1  13541  cvgcmp2nlemabs  13911  trilpolemisumle  13917  apdifflemr  13926  apdiff  13927