Theorem 2cnd 9109

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

Syntax hints:   → wi 4   ∈ wcel 2176  ℂcc 7923  2c2 9087

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187  ax-resscn 8017  ax-1re 8019  ax-addrcl 8022

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-in 3172  df-ss 3179  df-2 9095

This theorem is referenced by:  subhalfhalf  9272  cnm2m1cnm3  9289  xp1d2m1eqxm1d2  9290  nneo  9476  zeo2  9479  2tnp1ge0ge0  10444  flhalf  10445  fldiv4lem1div2uz2  10449  q2txmodxeq0  10529  mulbinom2  10801  binom3  10802  zesq  10803  sqoddm1div8  10838  mulsubdivbinom2ap  10856  cvg1nlemcxze  11293  resqrexlemover  11321  resqrexlemlo  11324  resqrexlemcalc1  11325  resqrexlemnm  11329  amgm2  11429  maxabslemab  11517  maxabslemlub  11518  max0addsup  11530  minabs  11547  bdtri  11551  trirecip  11812  geo2sum  11825  ege2le3  11982  efgt0  11995  tanval3ap  12025  even2n  12185  oddm1even  12186  oddp1even  12187  mulsucdiv2z  12196  ltoddhalfle  12204  m1exp1  12212  nn0enne  12213  flodddiv4  12247  flodddiv4t2lthalf  12250  bitsp1e  12263  bitsp1o  12264  bitsmod  12267  bitsinv1lem  12272  sqrt2irrlem  12483  sqrt2irr  12484  pw2dvdslemn  12487  pw2dvdseulemle  12489  oddpwdc  12496  sqrt2irraplemnn  12501  prmdiv  12557  pythagtriplem15  12601  pythagtriplem16  12602  pythagtriplem17  12603  4sqlem7  12707  4sqlem10  12710  4sqlem19  12732  2expltfac  12762  oddennn  12763  evenennn  12764  hoverb  15120  sin0pilem2  15254  perfectlem2  15472  perfect  15473  lgslem1  15477  gausslemma2dlem1a  15535  gausslemma2dlem1f1o  15537  gausslemma2dlem3  15540  gausslemma2dlem6  15544  lgseisenlem1  15547  lgseisenlem2  15548  lgseisenlem3  15549  lgseisenlem4  15550  lgsquadlem1  15554  lgsquadlem2  15555  lgsquad2lem1  15558  2lgslem1a1  15563  2lgslem1a2  15564  2lgslem1b  15566  2lgslem1c  15567  2lgslem3a1  15574  2lgslem3d1  15577  cvgcmp2nlemabs  15971  trilpolemisumle  15977  apdifflemr  15986  apdiff  15987