Theorem 0cnd 7949

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

Syntax hints:   → wi 4   ∈ wcel 2148  ℂcc 7808  0cc0 7810

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159  ax-1cn 7903  ax-icn 7905  ax-addcl 7906  ax-mulcl 7908  ax-i2m1 7915

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173

This theorem is referenced by:  mulap0r  8571  mulap0  8610  mul0eqap  8626  diveqap0  8638  eqneg  8688  div2subap  8793  prodgt0  8808  un0addcl  9208  un0mulcl  9209  modsumfzodifsn  10395  ser0  10513  ser0f  10514  abs00ap  11070  abs00  11072  abssubne0  11099  mul0inf  11248  clim0c  11293  sumrbdclem  11384  summodclem2a  11388  zsumdc  11391  fsum3  11394  isumz  11396  isumss  11398  fisumss  11399  fsum3cvg2  11401  fsum3ser  11404  fsumcl2lem  11405  fsumcl  11407  fsumadd  11413  fsumsplit  11414  sumsnf  11416  sumsplitdc  11439  fsummulc2  11455  ef0lem  11667  ef4p  11701  tanvalap  11715  modprm0  12253  pcmpt2  12341  4sqlem10  12384  fsumcncntop  14026  limcimolemlt  14103  dvmptcmulcn  14153  dveflem  14157  dvef  14158  ptolemy  14215  lgsdir2  14404  lgsdir  14406  apdiff  14766  iswomni0  14769