Theorem 0cnd 8162

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℂcc 8020  0cc0 8022

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211  ax-1cn 8115  ax-icn 8117  ax-addcl 8118  ax-mulcl 8120  ax-i2m1 8127

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  mulap0r  8785  mulap0  8824  mul0eqap  8840  diveqap0  8852  eqneg  8902  div2subap  9007  prodgt0  9022  un0addcl  9425  un0mulcl  9426  modsumfzodifsn  10648  ser0  10785  ser0f  10786  abs00ap  11613  abs00  11615  abssubne0  11642  mul0inf  11792  clim0c  11837  sumrbdclem  11928  summodclem2a  11932  zsumdc  11935  fsum3  11938  isumz  11940  isumss  11942  fisumss  11943  fsum3cvg2  11945  fsum3ser  11948  fsumcl2lem  11949  fsumcl  11951  fsumadd  11957  fsumsplit  11958  sumsnf  11960  sumsplitdc  11983  fsummulc2  11999  ef0lem  12211  ef4p  12245  tanvalap  12259  modprm0  12817  pcmpt2  12907  4sqlem10  12950  4sqlem11  12964  fsumcncntop  15281  limcimolemlt  15378  dvmptcmulcn  15435  dvmptfsum  15439  dveflem  15440  dvef  15441  plyf  15451  elplyr  15454  elplyd  15455  ply1term  15457  plyaddlem  15463  plymullem  15464  plycolemc  15472  plycn  15476  dvply1  15479  ptolemy  15538  lgsdir2  15752  lgsdir  15754  apdiff  16588  iswomni0  16591