Theorem 2cnd 8703

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

Syntax hints:   → wi 4   ∈ wcel 1463  ℂcc 7545  2c2 8681

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-11 1467  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-resscn 7637  ax-1re 7639  ax-addrcl 7642

This theorem depends on definitions:  df-bi 116  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-in 3043  df-ss 3050  df-2 8689

This theorem is referenced by:  cnm2m1cnm3  8875  xp1d2m1eqxm1d2  8876  nneo  9058  zeo2  9061  2tnp1ge0ge0  9967  flhalf  9968  q2txmodxeq0  10050  mulbinom2  10301  binom3  10302  zesq  10303  sqoddm1div8  10337  cvg1nlemcxze  10646  resqrexlemover  10674  resqrexlemlo  10677  resqrexlemcalc1  10678  resqrexlemnm  10682  amgm2  10782  maxabslemab  10870  maxabslemlub  10871  max0addsup  10883  minabs  10899  bdtri  10903  trirecip  11162  geo2sum  11175  ege2le3  11228  efgt0  11241  tanval3ap  11272  even2n  11419  oddm1even  11420  oddp1even  11421  mulsucdiv2z  11430  ltoddhalfle  11438  m1exp1  11446  nn0enne  11447  flodddiv4  11479  flodddiv4t2lthalf  11482  sqrt2irrlem  11685  sqrt2irr  11686  pw2dvdslemn  11688  pw2dvdseulemle  11690  oddpwdc  11697  sqrt2irraplemnn  11702  oddennn  11750  evenennn  11751  cvgcmp2nlemabs  12919  trilpolemisumle  12923