Theorem 2cnd 9379

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  ℂcc 8177  2c2 9357

This proof depends on 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 8271  ax-1re 8273  ax-addrcl 8276

This proof 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 9365

This theorem is used by:  subhalfhalf  9544  cnm2m1cnm3  9561  xp1d2m1eqxm1d2  9562  nneo  9753  zeo2  9756  2tnp1ge0ge0  10749  flhalf  10750  fldiv4lem1div2uz2  10754  q2txmodxeq0  10834  mulbinom2  11106  binom3  11107  zesq  11109  sqoddm1div8  11144  mulsubdivbinom2ap  11163  sq01  11674  cvg1nlemcxze  11762  resqrexlemover  11790  resqrexlemlo  11793  resqrexlemcalc1  11794  resqrexlemnm  11798  amgm2  11899  maxabslemab  11987  maxabslemlub  11988  max0addsup  12000  minabs  12017  bdtri  12022  trirecip  12284  geo2sum  12297  ege2le3  12454  efgt0  12467  tanval3ap  12497  even2n  12657  oddm1even  12658  oddp1even  12659  mulsucdiv2z  12668  ltoddhalfle  12676  m1exp1  12684  nn0enne  12685  flodddiv4  12719  flodddiv4t2lthalf  12722  bitsp1e  12735  bitsp1o  12736  bitsmod  12739  bitsinv1lem  12744  sqrt2irrlem  12956  sqrt2irr  12957  sqrt2irraplemnn  12975  prmdiv  13033  pythagtriplem15  13077  pythagtriplem16  13078  pythagtriplem17  13079  4sqlem7  13183  4sqlem10  13186  4sqlem19  13208  2expltfac  13239  oddennn  13332  evenennn  13333  hoverb  15798  sin0pilem2  15933  log2tlbndlog2  16139  perfectlem2  16198  perfect  16199  bcp1ctr  16204  bclbnd  16205  bposlem1  16209  bposlem2  16210  lgslem1  16217  gausslemma2dlem1a  16275  gausslemma2dlem1f1o  16277  gausslemma2dlem3  16280  gausslemma2dlem6  16284  lgseisenlem1  16287  lgseisenlem2  16288  lgseisenlem3  16289  lgseisenlem4  16290  lgsquadlem1  16294  lgsquadlem2  16295  lgsquad2lem1  16298  2lgslem1a1  16303  2lgslem1a2  16304  2lgslem1b  16306  2lgslem1c  16307  2lgslem3a1  16314  2lgslem3d1  16317  clwwlkext2edg  16761  clwwlknonex2lem1  16776  clwwlknonex2lem2  16777  cvgcmp2nlemabs  17179  trilpolemisumle  17185  apdifflemr  17194  apdiff  17195  qdiff  17196