Theorem 2cnd 8112

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

Syntax hints:   → wi 4   ∈ wcel 1433  ℂcc 6979  2c2 8089

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-11 1437  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063  ax-resscn 7068  ax-1re 7070  ax-addrcl 7073

This theorem depends on definitions:  df-bi 115  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-in 2979  df-ss 2986  df-2 8098

This theorem is referenced by:  cnm2m1cnm3  8282  xp1d2m1eqxm1d2  8283  nneo  8450  zeo2  8453  2tnp1ge0ge0  9303  flhalf  9304  q2txmodxeq0  9386  mulbinom2  9589  binom3  9590  zesq  9591  sqoddm1div8  9625  cvg1nlemcxze  9868  resqrexlemover  9896  resqrexlemlo  9899  resqrexlemcalc1  9900  resqrexlemnm  9904  amgm2  10004  maxabslemab  10092  maxabslemlub  10093  max0addsup  10105  even2n  10273  oddm1even  10274  oddp1even  10275  mulsucdiv2z  10285  ltoddhalfle  10293  m1exp1  10301  nn0enne  10302  flodddiv4  10334  flodddiv4t2lthalf  10337  sqrt2irrlem  10540  sqrt2irr  10541  pw2dvdslemn  10543  pw2dvdseulemle  10545  oddpwdc  10552  sqrt2irraplemnn  10557