Theorem 0cnd 8065

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

Syntax hints:   → wi 4   ∈ wcel 2176  ℂcc 7923  0cc0 7925

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-ext 2187  ax-1cn 8018  ax-icn 8020  ax-addcl 8021  ax-mulcl 8023  ax-i2m1 8030

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-clel 2201

This theorem is referenced by:  mulap0r  8688  mulap0  8727  mul0eqap  8743  diveqap0  8755  eqneg  8805  div2subap  8910  prodgt0  8925  un0addcl  9328  un0mulcl  9329  modsumfzodifsn  10541  ser0  10678  ser0f  10679  abs00ap  11373  abs00  11375  abssubne0  11402  mul0inf  11552  clim0c  11597  sumrbdclem  11688  summodclem2a  11692  zsumdc  11695  fsum3  11698  isumz  11700  isumss  11702  fisumss  11703  fsum3cvg2  11705  fsum3ser  11708  fsumcl2lem  11709  fsumcl  11711  fsumadd  11717  fsumsplit  11718  sumsnf  11720  sumsplitdc  11743  fsummulc2  11759  ef0lem  11971  ef4p  12005  tanvalap  12019  modprm0  12577  pcmpt2  12667  4sqlem10  12710  4sqlem11  12724  fsumcncntop  15039  limcimolemlt  15136  dvmptcmulcn  15193  dvmptfsum  15197  dveflem  15198  dvef  15199  plyf  15209  elplyr  15212  elplyd  15213  ply1term  15215  plyaddlem  15221  plymullem  15222  plycolemc  15230  plycn  15234  dvply1  15237  ptolemy  15296  lgsdir2  15510  lgsdir  15512  apdiff  15987  iswomni0  15990