Theorem 0cnd 8172

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

Syntax hints:   → wi 4   ∈ wcel 2202  ℂcc 8030  0cc0 8032

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213  ax-1cn 8125  ax-icn 8127  ax-addcl 8128  ax-mulcl 8130  ax-i2m1 8137

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

This theorem is referenced by:  mulap0r  8795  mulap0  8834  mul0eqap  8850  diveqap0  8862  eqneg  8912  div2subap  9017  prodgt0  9032  un0addcl  9435  un0mulcl  9436  modsumfzodifsn  10659  ser0  10796  ser0f  10797  abs00ap  11627  abs00  11629  abssubne0  11656  mul0inf  11806  clim0c  11851  sumrbdclem  11943  summodclem2a  11947  zsumdc  11950  fsum3  11953  isumz  11955  isumss  11957  fisumss  11958  fsum3cvg2  11960  fsum3ser  11963  fsumcl2lem  11964  fsumcl  11966  fsumadd  11972  fsumsplit  11973  sumsnf  11975  sumsplitdc  11998  fsummulc2  12014  ef0lem  12226  ef4p  12260  tanvalap  12274  modprm0  12832  pcmpt2  12922  4sqlem10  12965  4sqlem11  12979  fsumcncntop  15297  limcimolemlt  15394  dvmptcmulcn  15451  dvmptfsum  15455  dveflem  15456  dvef  15457  plyf  15467  elplyr  15470  elplyd  15471  ply1term  15473  plyaddlem  15479  plymullem  15480  plycolemc  15488  plycn  15492  dvply1  15495  ptolemy  15554  lgsdir2  15768  lgsdir  15770  apdiff  16678  iswomni0  16682