Theorem 2cnd 8951

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

Syntax hints:   → wi 4   ∈ wcel 2141  ℂcc 7772  2c2 8929

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 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152  ax-resscn 7866  ax-1re 7868  ax-addrcl 7871

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-in 3127  df-ss 3134  df-2 8937

This theorem is referenced by:  cnm2m1cnm3  9129  xp1d2m1eqxm1d2  9130  nneo  9315  zeo2  9318  2tnp1ge0ge0  10257  flhalf  10258  q2txmodxeq0  10340  mulbinom2  10592  binom3  10593  zesq  10594  sqoddm1div8  10629  cvg1nlemcxze  10946  resqrexlemover  10974  resqrexlemlo  10977  resqrexlemcalc1  10978  resqrexlemnm  10982  amgm2  11082  maxabslemab  11170  maxabslemlub  11171  max0addsup  11183  minabs  11199  bdtri  11203  trirecip  11464  geo2sum  11477  ege2le3  11634  efgt0  11647  tanval3ap  11677  even2n  11833  oddm1even  11834  oddp1even  11835  mulsucdiv2z  11844  ltoddhalfle  11852  m1exp1  11860  nn0enne  11861  flodddiv4  11893  flodddiv4t2lthalf  11896  sqrt2irrlem  12115  sqrt2irr  12116  pw2dvdslemn  12119  pw2dvdseulemle  12121  oddpwdc  12128  sqrt2irraplemnn  12133  prmdiv  12189  pythagtriplem15  12232  pythagtriplem16  12233  pythagtriplem17  12234  4sqlem7  12336  4sqlem10  12339  oddennn  12347  evenennn  12348  sin0pilem2  13497  lgslem1  13695  cvgcmp2nlemabs  14064  trilpolemisumle  14070  apdifflemr  14079  apdiff  14080