Theorem 0cnd 7950

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

Syntax hints:   → wi 4   ∈ wcel 2148  ℂcc 7809  0cc0 7811

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 7904  ax-icn 7906  ax-addcl 7907  ax-mulcl 7909  ax-i2m1 7916

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

This theorem is referenced by:  mulap0r  8572  mulap0  8611  mul0eqap  8627  diveqap0  8639  eqneg  8689  div2subap  8794  prodgt0  8809  un0addcl  9209  un0mulcl  9210  modsumfzodifsn  10396  ser0  10514  ser0f  10515  abs00ap  11071  abs00  11073  abssubne0  11100  mul0inf  11249  clim0c  11294  sumrbdclem  11385  summodclem2a  11389  zsumdc  11392  fsum3  11395  isumz  11397  isumss  11399  fisumss  11400  fsum3cvg2  11402  fsum3ser  11405  fsumcl2lem  11406  fsumcl  11408  fsumadd  11414  fsumsplit  11415  sumsnf  11417  sumsplitdc  11440  fsummulc2  11456  ef0lem  11668  ef4p  11702  tanvalap  11716  modprm0  12254  pcmpt2  12342  4sqlem10  12385  fsumcncntop  14059  limcimolemlt  14136  dvmptcmulcn  14186  dveflem  14190  dvef  14191  ptolemy  14248  lgsdir2  14437  lgsdir  14439  apdiff  14799  iswomni0  14802