Theorem 0cnd 8283

Description: 0 is a complex number, deductive form. (Contributed by David A. Wheeler, 8-Dec-2018.)

Assertion

Ref	Expression
0cnd	⊢ (𝜑 → 0 ∈ ℂ)

Proof of Theorem 0cnd

Step	Hyp	Ref	Expression
1		0cn 8282	. 2 ⊢ 0 ∈ ℂ
2	1	a1i 9	1 ⊢ (𝜑 → 0 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2205  ℂcc 8141  0cc0 8143

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-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2216  ax-1cn 8236  ax-icn 8238  ax-addcl 8239  ax-mulcl 8241  ax-i2m1 8248

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-clel 2230

This theorem is referenced by:  addeq0  8666  mulap0r  8906  mulap0  8945  mul0eqap  8961  diveqap0  8973  eqneg  9023  div2subap  9128  prodgt0  9143  un0addcl  9546  un0mulcl  9547  modsumfzodifsn  10782  ser0  10919  ser0f  10920  resq01  11044  abs00ap  11772  abs00  11774  abssubne0  11801  mul0inf  11951  clim0c  11996  sumrbdclem  12088  summodclem2a  12092  zsumdc  12095  fsum3  12098  isumz  12100  isumss  12102  fisumss  12103  fsum3cvg2  12105  fsum3ser  12108  fsumcl2lem  12109  fsumcl  12111  fsumadd  12117  fsumsplit  12118  sumsnf  12120  sumsplitdc  12143  fsummulc2  12159  ef0lem  12371  ef4p  12405  tanvalap  12419  modprm0  12977  pcmpt2  13067  4sqlem10  13110  4sqlem11  13124  ballotfilemic  13194  ballotfilem1c  13195  fsumcncntop  15558  limcimolemlt  15655  dvmptcmulcn  15712  dvmptfsum  15716  dveflem  15717  dvef  15718  plyf  15728  elplyr  15731  elplyd  15732  ply1term  15734  plyaddlem  15740  plymullem  15741  plycolemc  15749  plycn  15753  dvply1  15756  ptolemy  15815  lgsdir2  16032  lgsdir  16034  apdiff  16958  iswomni0  16962  trimul0or  16971