Theorem 0cnd 7888

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

Syntax hints:   → wi 4   ∈ wcel 2136  ℂcc 7747  0cc0 7749

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522  ax-ext 2147  ax-1cn 7842  ax-icn 7844  ax-addcl 7845  ax-mulcl 7847  ax-i2m1 7854

This theorem depends on definitions:  df-bi 116  df-cleq 2158  df-clel 2161

This theorem is referenced by:  mulap0r  8509  mulap0  8547  mul0eqap  8563  diveqap0  8574  eqneg  8624  div2subap  8729  prodgt0  8743  un0addcl  9143  un0mulcl  9144  modsumfzodifsn  10327  ser0  10445  ser0f  10446  abs00ap  11000  abs00  11002  abssubne0  11029  mul0inf  11178  clim0c  11223  sumrbdclem  11314  summodclem2a  11318  zsumdc  11321  fsum3  11324  isumz  11326  isumss  11328  fisumss  11329  fsum3cvg2  11331  fsum3ser  11334  fsumcl2lem  11335  fsumcl  11337  fsumadd  11343  fsumsplit  11344  sumsnf  11346  sumsplitdc  11369  fsummulc2  11385  ef0lem  11597  ef4p  11631  tanvalap  11645  modprm0  12182  pcmpt2  12270  4sqlem10  12313  fsumcncntop  13156  limcimolemlt  13233  dvmptcmulcn  13283  dveflem  13287  dvef  13288  ptolemy  13345  lgsdir2  13534  lgsdir  13536  apdiff  13887  iswomni0  13890