Theorem 2cnd 9006

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

Syntax hints:   → wi 4   ∈ wcel 2158  ℂcc 7823  2c2 8984

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 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-11 1516  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169  ax-resscn 7917  ax-1re 7919  ax-addrcl 7922

This theorem depends on definitions:  df-bi 117  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-in 3147  df-ss 3154  df-2 8992

This theorem is referenced by:  cnm2m1cnm3  9184  xp1d2m1eqxm1d2  9185  nneo  9370  zeo2  9373  2tnp1ge0ge0  10315  flhalf  10316  q2txmodxeq0  10398  mulbinom2  10651  binom3  10652  zesq  10653  sqoddm1div8  10688  mulsubdivbinom2ap  10705  cvg1nlemcxze  11005  resqrexlemover  11033  resqrexlemlo  11036  resqrexlemcalc1  11037  resqrexlemnm  11041  amgm2  11141  maxabslemab  11229  maxabslemlub  11230  max0addsup  11242  minabs  11258  bdtri  11262  trirecip  11523  geo2sum  11536  ege2le3  11693  efgt0  11706  tanval3ap  11736  even2n  11893  oddm1even  11894  oddp1even  11895  mulsucdiv2z  11904  ltoddhalfle  11912  m1exp1  11920  nn0enne  11921  flodddiv4  11953  flodddiv4t2lthalf  11956  sqrt2irrlem  12175  sqrt2irr  12176  pw2dvdslemn  12179  pw2dvdseulemle  12181  oddpwdc  12188  sqrt2irraplemnn  12193  prmdiv  12249  pythagtriplem15  12292  pythagtriplem16  12293  pythagtriplem17  12294  4sqlem7  12396  4sqlem10  12399  oddennn  12407  evenennn  12408  sin0pilem2  14556  lgslem1  14754  lgseisenlem1  14803  lgseisenlem2  14804  cvgcmp2nlemabs  15134  trilpolemisumle  15140  apdifflemr  15149  apdiff  15150