Theorem 2cnd 8986

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

Syntax hints:   → wi 4   ∈ wcel 2148  ℂcc 7804  2c2 8964

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-resscn 7898  ax-1re 7900  ax-addrcl 7903

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3135  df-ss 3142  df-2 8972

This theorem is referenced by:  cnm2m1cnm3  9164  xp1d2m1eqxm1d2  9165  nneo  9350  zeo2  9353  2tnp1ge0ge0  10294  flhalf  10295  q2txmodxeq0  10377  mulbinom2  10629  binom3  10630  zesq  10631  sqoddm1div8  10666  cvg1nlemcxze  10982  resqrexlemover  11010  resqrexlemlo  11013  resqrexlemcalc1  11014  resqrexlemnm  11018  amgm2  11118  maxabslemab  11206  maxabslemlub  11207  max0addsup  11219  minabs  11235  bdtri  11239  trirecip  11500  geo2sum  11513  ege2le3  11670  efgt0  11683  tanval3ap  11713  even2n  11869  oddm1even  11870  oddp1even  11871  mulsucdiv2z  11880  ltoddhalfle  11888  m1exp1  11896  nn0enne  11897  flodddiv4  11929  flodddiv4t2lthalf  11932  sqrt2irrlem  12151  sqrt2irr  12152  pw2dvdslemn  12155  pw2dvdseulemle  12157  oddpwdc  12164  sqrt2irraplemnn  12169  prmdiv  12225  pythagtriplem15  12268  pythagtriplem16  12269  pythagtriplem17  12270  4sqlem7  12372  4sqlem10  12375  oddennn  12383  evenennn  12384  sin0pilem2  13985  lgslem1  14183  cvgcmp2nlemabs  14551  trilpolemisumle  14557  apdifflemr  14566  apdiff  14567