Theorem 2cnd 9310

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

Syntax hints:   → wi 4   ∈ wcel 2203  ℂcc 8125  2c2 9288

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214  ax-resscn 8219  ax-1re 8221  ax-addrcl 8224

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-in 3217  df-ss 3224  df-2 9296

This theorem is referenced by:  subhalfhalf  9473  cnm2m1cnm3  9490  xp1d2m1eqxm1d2  9491  nneo  9681  zeo2  9684  2tnp1ge0ge0  10661  flhalf  10662  fldiv4lem1div2uz2  10666  q2txmodxeq0  10746  mulbinom2  11018  binom3  11019  zesq  11020  sqoddm1div8  11055  mulsubdivbinom2ap  11073  cvg1nlemcxze  11667  resqrexlemover  11695  resqrexlemlo  11698  resqrexlemcalc1  11699  resqrexlemnm  11703  amgm2  11803  maxabslemab  11891  maxabslemlub  11892  max0addsup  11904  minabs  11921  bdtri  11925  trirecip  12187  geo2sum  12200  ege2le3  12357  efgt0  12370  tanval3ap  12400  even2n  12560  oddm1even  12561  oddp1even  12562  mulsucdiv2z  12571  ltoddhalfle  12579  m1exp1  12587  nn0enne  12588  flodddiv4  12622  flodddiv4t2lthalf  12625  bitsp1e  12638  bitsp1o  12639  bitsmod  12642  bitsinv1lem  12647  sqrt2irrlem  12858  sqrt2irr  12859  pw2dvdslemn  12862  pw2dvdseulemle  12864  oddpwdc  12871  sqrt2irraplemnn  12876  prmdiv  12932  pythagtriplem15  12976  pythagtriplem16  12977  pythagtriplem17  12978  4sqlem7  13082  4sqlem10  13085  4sqlem19  13107  2expltfac  13137  oddennn  13143  evenennn  13144  hoverb  15513  sin0pilem2  15647  perfectlem2  15868  perfect  15869  lgslem1  15873  gausslemma2dlem1a  15931  gausslemma2dlem1f1o  15933  gausslemma2dlem3  15936  gausslemma2dlem6  15940  lgseisenlem1  15943  lgseisenlem2  15944  lgseisenlem3  15945  lgseisenlem4  15946  lgsquadlem1  15950  lgsquadlem2  15951  lgsquad2lem1  15954  2lgslem1a1  15959  2lgslem1a2  15960  2lgslem1b  15962  2lgslem1c  15963  2lgslem3a1  15970  2lgslem3d1  15973  clwwlkext2edg  16417  clwwlknonex2lem1  16432  clwwlknonex2lem2  16433  cvgcmp2nlemabs  16816  trilpolemisumle  16822  apdifflemr  16831  apdiff  16832  qdiff  16833