Theorem 0cnd 7752

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

Syntax hints:   → wi 4   ∈ wcel 1480  ℂcc 7611  0cc0 7613

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2119  ax-1cn 7706  ax-icn 7708  ax-addcl 7709  ax-mulcl 7711  ax-i2m1 7718

This theorem depends on definitions:  df-bi 116  df-cleq 2130  df-clel 2133

This theorem is referenced by:  mulap0r  8370  mulap0  8408  mul0eqap  8424  diveqap0  8435  eqneg  8485  div2subap  8589  prodgt0  8603  un0addcl  9003  un0mulcl  9004  modsumfzodifsn  10162  ser0  10280  ser0f  10281  abs00ap  10827  abs00  10829  abssubne0  10856  mul0inf  11005  clim0c  11048  sumrbdclem  11138  summodclem2a  11143  zsumdc  11146  fsum3  11149  isumz  11151  isumss  11153  fisumss  11154  fsum3cvg2  11156  fsum3ser  11159  fsumcl2lem  11160  fsumcl  11162  fsumadd  11168  fsumsplit  11169  sumsnf  11171  sumsplitdc  11194  fsummulc2  11210  ef0lem  11355  ef4p  11389  tanvalap  11404  fsumcncntop  12714  limcimolemlt  12791  dvmptcmulcn  12841  dveflem  12844  dvef  12845  ptolemy  12894