Theorem 0cnd 7759

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

Syntax hints:   → wi 4   ∈ wcel 1480  ℂcc 7618  0cc0 7620

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 2121  ax-1cn 7713  ax-icn 7715  ax-addcl 7716  ax-mulcl 7718  ax-i2m1 7725

This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135

This theorem is referenced by:  mulap0r  8377  mulap0  8415  mul0eqap  8431  diveqap0  8442  eqneg  8492  div2subap  8596  prodgt0  8610  un0addcl  9010  un0mulcl  9011  modsumfzodifsn  10169  ser0  10287  ser0f  10288  abs00ap  10834  abs00  10836  abssubne0  10863  mul0inf  11012  clim0c  11055  sumrbdclem  11146  summodclem2a  11150  zsumdc  11153  fsum3  11156  isumz  11158  isumss  11160  fisumss  11161  fsum3cvg2  11163  fsum3ser  11166  fsumcl2lem  11167  fsumcl  11169  fsumadd  11175  fsumsplit  11176  sumsnf  11178  sumsplitdc  11201  fsummulc2  11217  ef0lem  11366  ef4p  11400  tanvalap  11415  fsumcncntop  12725  limcimolemlt  12802  dvmptcmulcn  12852  dveflem  12855  dvef  12856  ptolemy  12905