Theorem 2cnd 9258

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

Syntax hints:   → wi 4   ∈ wcel 2202  ℂcc 8073  2c2 9236

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213  ax-resscn 8167  ax-1re 8169  ax-addrcl 8172

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214  df-2 9244

This theorem is referenced by:  subhalfhalf  9421  cnm2m1cnm3  9438  xp1d2m1eqxm1d2  9439  nneo  9627  zeo2  9630  2tnp1ge0ge0  10607  flhalf  10608  fldiv4lem1div2uz2  10612  q2txmodxeq0  10692  mulbinom2  10964  binom3  10965  zesq  10966  sqoddm1div8  11001  mulsubdivbinom2ap  11019  cvg1nlemcxze  11605  resqrexlemover  11633  resqrexlemlo  11636  resqrexlemcalc1  11637  resqrexlemnm  11641  amgm2  11741  maxabslemab  11829  maxabslemlub  11830  max0addsup  11842  minabs  11859  bdtri  11863  trirecip  12125  geo2sum  12138  ege2le3  12295  efgt0  12308  tanval3ap  12338  even2n  12498  oddm1even  12499  oddp1even  12500  mulsucdiv2z  12509  ltoddhalfle  12517  m1exp1  12525  nn0enne  12526  flodddiv4  12560  flodddiv4t2lthalf  12563  bitsp1e  12576  bitsp1o  12577  bitsmod  12580  bitsinv1lem  12585  sqrt2irrlem  12796  sqrt2irr  12797  pw2dvdslemn  12800  pw2dvdseulemle  12802  oddpwdc  12809  sqrt2irraplemnn  12814  prmdiv  12870  pythagtriplem15  12914  pythagtriplem16  12915  pythagtriplem17  12916  4sqlem7  13020  4sqlem10  13023  4sqlem19  13045  2expltfac  13075  oddennn  13076  evenennn  13077  hoverb  15442  sin0pilem2  15576  perfectlem2  15797  perfect  15798  lgslem1  15802  gausslemma2dlem1a  15860  gausslemma2dlem1f1o  15862  gausslemma2dlem3  15865  gausslemma2dlem6  15869  lgseisenlem1  15872  lgseisenlem2  15873  lgseisenlem3  15874  lgseisenlem4  15875  lgsquadlem1  15879  lgsquadlem2  15880  lgsquad2lem1  15883  2lgslem1a1  15888  2lgslem1a2  15889  2lgslem1b  15891  2lgslem1c  15892  2lgslem3a1  15899  2lgslem3d1  15902  clwwlkext2edg  16346  clwwlknonex2lem1  16361  clwwlknonex2lem2  16362  cvgcmp2nlemabs  16747  trilpolemisumle  16753  apdifflemr  16762  apdiff  16763  qdiff  16764