Theorem 2cnd 9356

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

Syntax hints:   → wi 4   ∈ wcel 2209  ℂcc 8167  2c2 9334

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 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-resscn 8261  ax-1re 8263  ax-addrcl 8266

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233  df-2 9342

This theorem is referenced by:  subhalfhalf  9519  cnm2m1cnm3  9536  xp1d2m1eqxm1d2  9537  nneo  9728  zeo2  9731  2tnp1ge0ge0  10714  flhalf  10715  fldiv4lem1div2uz2  10719  q2txmodxeq0  10799  mulbinom2  11071  binom3  11072  zesq  11074  sqoddm1div8  11109  mulsubdivbinom2ap  11127  sq01  11638  cvg1nlemcxze  11726  resqrexlemover  11754  resqrexlemlo  11757  resqrexlemcalc1  11758  resqrexlemnm  11762  amgm2  11862  maxabslemab  11950  maxabslemlub  11951  max0addsup  11963  minabs  11980  bdtri  11984  trirecip  12246  geo2sum  12259  ege2le3  12416  efgt0  12429  tanval3ap  12459  even2n  12619  oddm1even  12620  oddp1even  12621  mulsucdiv2z  12630  ltoddhalfle  12638  m1exp1  12646  nn0enne  12647  flodddiv4  12681  flodddiv4t2lthalf  12684  bitsp1e  12697  bitsp1o  12698  bitsmod  12701  bitsinv1lem  12706  sqrt2irrlem  12917  sqrt2irr  12918  pw2dvdslemn  12921  pw2dvdseulemle  12923  oddpwdc  12930  sqrt2irraplemnn  12935  prmdiv  12991  pythagtriplem15  13035  pythagtriplem16  13036  pythagtriplem17  13037  4sqlem7  13141  4sqlem10  13144  4sqlem19  13166  2expltfac  13196  oddennn  13261  evenennn  13262  hoverb  15672  sin0pilem2  15806  perfectlem2  16028  perfect  16029  lgslem1  16033  gausslemma2dlem1a  16091  gausslemma2dlem1f1o  16093  gausslemma2dlem3  16096  gausslemma2dlem6  16100  lgseisenlem1  16103  lgseisenlem2  16104  lgseisenlem3  16105  lgseisenlem4  16106  lgsquadlem1  16110  lgsquadlem2  16111  lgsquad2lem1  16114  2lgslem1a1  16119  2lgslem1a2  16120  2lgslem1b  16122  2lgslem1c  16123  2lgslem3a1  16130  2lgslem3d1  16133  clwwlkext2edg  16577  clwwlknonex2lem1  16592  clwwlknonex2lem2  16593  cvgcmp2nlemabs  16986  trilpolemisumle  16992  apdifflemr  17001  apdiff  17002  qdiff  17003