Theorem 2cnd 8793

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

Syntax hints:   → wi 4   ∈ wcel 1480  ℂcc 7618  2c2 8771

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-resscn 7712  ax-1re 7714  ax-addrcl 7717

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-in 3077  df-ss 3084  df-2 8779

This theorem is referenced by:  cnm2m1cnm3  8971  xp1d2m1eqxm1d2  8972  nneo  9154  zeo2  9157  2tnp1ge0ge0  10074  flhalf  10075  q2txmodxeq0  10157  mulbinom2  10408  binom3  10409  zesq  10410  sqoddm1div8  10444  cvg1nlemcxze  10754  resqrexlemover  10782  resqrexlemlo  10785  resqrexlemcalc1  10786  resqrexlemnm  10790  amgm2  10890  maxabslemab  10978  maxabslemlub  10979  max0addsup  10991  minabs  11007  bdtri  11011  trirecip  11270  geo2sum  11283  ege2le3  11377  efgt0  11390  tanval3ap  11421  even2n  11571  oddm1even  11572  oddp1even  11573  mulsucdiv2z  11582  ltoddhalfle  11590  m1exp1  11598  nn0enne  11599  flodddiv4  11631  flodddiv4t2lthalf  11634  sqrt2irrlem  11839  sqrt2irr  11840  pw2dvdslemn  11843  pw2dvdseulemle  11845  oddpwdc  11852  sqrt2irraplemnn  11857  oddennn  11905  evenennn  11906  sin0pilem2  12863  cvgcmp2nlemabs  13227  trilpolemisumle  13231