Theorem 0cnd 8215

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

Syntax hints:   → wi 4   ∈ wcel 2202  ℂcc 8073  0cc0 8075

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 2213  ax-1cn 8168  ax-icn 8170  ax-addcl 8171  ax-mulcl 8173  ax-i2m1 8180

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

This theorem is referenced by:  mulap0r  8837  mulap0  8876  mul0eqap  8892  diveqap0  8904  eqneg  8954  div2subap  9059  prodgt0  9074  un0addcl  9477  un0mulcl  9478  modsumfzodifsn  10704  ser0  10841  ser0f  10842  abs00ap  11685  abs00  11687  abssubne0  11714  mul0inf  11864  clim0c  11909  sumrbdclem  12001  summodclem2a  12005  zsumdc  12008  fsum3  12011  isumz  12013  isumss  12015  fisumss  12016  fsum3cvg2  12018  fsum3ser  12021  fsumcl2lem  12022  fsumcl  12024  fsumadd  12030  fsumsplit  12031  sumsnf  12033  sumsplitdc  12056  fsummulc2  12072  ef0lem  12284  ef4p  12318  tanvalap  12332  modprm0  12890  pcmpt2  12980  4sqlem10  13023  4sqlem11  13037  fsumcncntop  15361  limcimolemlt  15458  dvmptcmulcn  15515  dvmptfsum  15519  dveflem  15520  dvef  15521  plyf  15531  elplyr  15534  elplyd  15535  ply1term  15537  plyaddlem  15543  plymullem  15544  plycolemc  15552  plycn  15556  dvply1  15559  ptolemy  15618  lgsdir2  15835  lgsdir  15837  apdiff  16763  iswomni0  16767