Theorem 0cnd 8019

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

Syntax hints:   → wi 4   ∈ wcel 2167  ℂcc 7877  0cc0 7879

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178  ax-1cn 7972  ax-icn 7974  ax-addcl 7975  ax-mulcl 7977  ax-i2m1 7984

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-clel 2192

This theorem is referenced by:  mulap0r  8642  mulap0  8681  mul0eqap  8697  diveqap0  8709  eqneg  8759  div2subap  8864  prodgt0  8879  un0addcl  9282  un0mulcl  9283  modsumfzodifsn  10488  ser0  10625  ser0f  10626  abs00ap  11227  abs00  11229  abssubne0  11256  mul0inf  11406  clim0c  11451  sumrbdclem  11542  summodclem2a  11546  zsumdc  11549  fsum3  11552  isumz  11554  isumss  11556  fisumss  11557  fsum3cvg2  11559  fsum3ser  11562  fsumcl2lem  11563  fsumcl  11565  fsumadd  11571  fsumsplit  11572  sumsnf  11574  sumsplitdc  11597  fsummulc2  11613  ef0lem  11825  ef4p  11859  tanvalap  11873  modprm0  12423  pcmpt2  12513  4sqlem10  12556  4sqlem11  12570  fsumcncntop  14803  limcimolemlt  14900  dvmptcmulcn  14957  dvmptfsum  14961  dveflem  14962  dvef  14963  plyf  14973  elplyr  14976  elplyd  14977  ply1term  14979  plyaddlem  14985  plymullem  14986  plycolemc  14994  plycn  14998  dvply1  15001  ptolemy  15060  lgsdir2  15274  lgsdir  15276  apdiff  15692  iswomni0  15695