Theorem 1cnd 7043

Description: 1 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)

Assertion

Ref	Expression
1cnd	⊢ (𝜑 → 1 ∈ ℂ)

Proof of Theorem 1cnd

Step	Hyp	Ref	Expression
1		ax-1cn 6977	. 2 ⊢ 1 ∈ ℂ
2	1	a1i 9	1 ⊢ (𝜑 → 1 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 1393  ℂcc 6887  1c1 6890

This theorem was proved from axioms:  ax-1 5  ax-mp 7  ax-1cn 6977

This theorem is referenced by:  recrecap  7685  rec11ap  7686  rec11rap  7687  rerecclap  7706  recp1lt1  7865  nn1m1nn  7932  add1p1  8174  sub1m1  8175  cnm2m1cnm3  8176  div4p1lem1div2  8177  peano2z  8281  zaddcllempos  8282  peano2zm  8283  zaddcllemneg  8284  nn0n0n1ge2  8311  zneo  8339  peano5uzti  8346  lincmb01cmp  8871  iccf1o  8872  zpnn0elfzo1  9064  ubmelm1fzo  9082  fzoshftral  9094  qbtwnzlemstep  9103  rebtwn2zlemstep  9107  qbtwnrelemcalc  9110  flqaddz  9139  2tnp1ge0ge0  9143  ceiqm1l  9153  binom3  9366  zesq  9367  resqrexlemover  9608  absexpzap  9676