Theorem 0cnd 7578

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

Syntax hints:   → wi 4   ∈ wcel 1445  ℂcc 7445  0cc0 7447

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-4 1452  ax-17 1471  ax-ial 1479  ax-ext 2077  ax-1cn 7535  ax-icn 7537  ax-addcl 7538  ax-mulcl 7540  ax-i2m1 7547

This theorem depends on definitions:  df-bi 116  df-cleq 2088  df-clel 2091

This theorem is referenced by:  mulap0r  8189  mulap0  8220  diveqap0  8246  eqneg  8296  div2subap  8399  prodgt0  8410  un0addcl  8804  un0mulcl  8805  modsumfzodifsn  9952  ser0  10080  ser0f  10081  abs00ap  10626  abssubne0  10655  clim0c  10845  sumrbdclem  10934  summodclem2a  10939  zsumdc  10942  fsum3  10945  isumz  10947  isumss  10949  fisumss  10950  fsum3cvg2  10952  fsum3ser  10955  fsumcl2lem  10956  fsumcl  10958  fsumadd  10964  fsumsplit  10965  sumsnf  10967  sumsplitdc  10990  fsummulc2  11006  ef0lem  11114  ef4p  11148  tanvalap  11163