Theorem 0cnd 8171

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

Syntax hints:   → wi 4   ∈ wcel 2202  ℂcc 8029  0cc0 8031

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 8124  ax-icn 8126  ax-addcl 8127  ax-mulcl 8129  ax-i2m1 8136

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

This theorem is referenced by:  mulap0r  8794  mulap0  8833  mul0eqap  8849  diveqap0  8861  eqneg  8911  div2subap  9016  prodgt0  9031  un0addcl  9434  un0mulcl  9435  modsumfzodifsn  10657  ser0  10794  ser0f  10795  abs00ap  11622  abs00  11624  abssubne0  11651  mul0inf  11801  clim0c  11846  sumrbdclem  11937  summodclem2a  11941  zsumdc  11944  fsum3  11947  isumz  11949  isumss  11951  fisumss  11952  fsum3cvg2  11954  fsum3ser  11957  fsumcl2lem  11958  fsumcl  11960  fsumadd  11966  fsumsplit  11967  sumsnf  11969  sumsplitdc  11992  fsummulc2  12008  ef0lem  12220  ef4p  12254  tanvalap  12268  modprm0  12826  pcmpt2  12916  4sqlem10  12959  4sqlem11  12973  fsumcncntop  15290  limcimolemlt  15387  dvmptcmulcn  15444  dvmptfsum  15448  dveflem  15449  dvef  15450  plyf  15460  elplyr  15463  elplyd  15464  ply1term  15466  plyaddlem  15472  plymullem  15473  plycolemc  15481  plycn  15485  dvply1  15488  ptolemy  15547  lgsdir2  15761  lgsdir  15763  apdiff  16652  iswomni0  16655