Theorem 0cnd 8309

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

Syntax hints:   → wi 4   ∈ wcel 2209  ℂcc 8167  0cc0 8169

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220  ax-1cn 8262  ax-icn 8264  ax-addcl 8265  ax-mulcl 8267  ax-i2m1 8274

This theorem depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is referenced by:  addeq0  8693  mulap0r  8933  mulap0  8972  msq0  8987  mul0eqap  8990  diveqap0  9002  eqneg  9052  div2subap  9157  prodgt0  9172  un0addcl  9575  un0mulcl  9576  modsumfzodifsn  10811  ser0  10948  ser0f  10949  resq01  11073  sq01  11638  abs00ap  11806  abs00  11808  abssubne0  11835  mul0inf  11985  clim0c  12030  sumrbdclem  12122  summodclem2a  12126  zsumdc  12129  fsum3  12132  isumz  12134  isumss  12136  fisumss  12137  fsum3cvg2  12139  fsum3ser  12142  fsumcl2lem  12143  fsumcl  12145  fsumadd  12151  fsumsplit  12152  sumsnf  12154  sumsplitdc  12177  fsummulc2  12193  ef0lem  12405  ef4p  12439  tanvalap  12453  modprm0  13011  pcmpt2  13101  4sqlem10  13144  4sqlem11  13158  ballotfilemic  13228  ballotfilem1c  13229  fsumcncntop  15591  limcimolemlt  15688  dvmptcmulcn  15745  dvmptfsum  15749  dveflem  15750  dvef  15751  plyf  15761  elplyr  15764  elplyd  15765  ply1term  15767  plyaddlem  15773  plymullem  15774  plycolemc  15782  plycn  15786  dvply1  15789  ptolemy  15848  lgsdir2  16066  lgsdir  16068  apdiff  17002  iswomni0  17006