Theorem 0cnd 7913

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

Syntax hints:   → wi 4   ∈ wcel 2141  ℂcc 7772  0cc0 7774

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 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-ext 2152  ax-1cn 7867  ax-icn 7869  ax-addcl 7870  ax-mulcl 7872  ax-i2m1 7879

This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-clel 2166

This theorem is referenced by:  mulap0r  8534  mulap0  8572  mul0eqap  8588  diveqap0  8599  eqneg  8649  div2subap  8754  prodgt0  8768  un0addcl  9168  un0mulcl  9169  modsumfzodifsn  10352  ser0  10470  ser0f  10471  abs00ap  11026  abs00  11028  abssubne0  11055  mul0inf  11204  clim0c  11249  sumrbdclem  11340  summodclem2a  11344  zsumdc  11347  fsum3  11350  isumz  11352  isumss  11354  fisumss  11355  fsum3cvg2  11357  fsum3ser  11360  fsumcl2lem  11361  fsumcl  11363  fsumadd  11369  fsumsplit  11370  sumsnf  11372  sumsplitdc  11395  fsummulc2  11411  ef0lem  11623  ef4p  11657  tanvalap  11671  modprm0  12208  pcmpt2  12296  4sqlem10  12339  fsumcncntop  13350  limcimolemlt  13427  dvmptcmulcn  13477  dveflem  13481  dvef  13482  ptolemy  13539  lgsdir2  13728  lgsdir  13730  apdiff  14080  iswomni0  14083