Theorem 1cnd 7135

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

Assertion

Ref	Expression
1cnd	|- ( ph -> 1 e. CC )

Proof of Theorem 1cnd

Step	Hyp	Ref	Expression
1		ax-1cn 7069	. 2 |- 1 e. CC
2	1	a1i 9	1 |- ( ph -> 1 e. CC )

Syntax hints:   -> wi 4   e. wcel 1433   CCcc 6979   1c1 6982

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

This theorem is referenced by:  adddirp1d  7145  muladd11r  7264  recrecap  7797  rec11ap  7798  rec11rap  7799  rerecclap  7818  recp1lt1  7977  nn1m1nn  8057  add1p1  8280  sub1m1  8281  cnm2m1cnm3  8282  xp1d2m1eqxm1d2  8283  div4p1lem1div2  8284  peano2z  8387  zaddcllempos  8388  peano2zm  8389  zaddcllemneg  8390  nn0n0n1ge2  8418  zneo  8448  peano5uzti  8455  lincmb01cmp  9025  iccf1o  9026  zpnn0elfzo1  9217  ubmelm1fzo  9235  fzoshftral  9247  qbtwnzlemstep  9257  rebtwn2zlemstep  9261  qbtwnrelemcalc  9264  flqaddz  9299  2tnp1ge0ge0  9303  ceiqm1l  9313  qnegmod  9371  addmodlteq  9400  uzsinds  9428  binom3  9590  zesq  9591  sqoddm1div8  9625  nn0opthlem1d  9647  bcm1k  9687  bcp1n  9688  bcp1m1  9692  bcpasc  9693  bcn2m1  9696  resqrexlemover  9896  absexpzap  9966  zeo3  10267  oddm1even  10274  oddp1even  10275  oexpneg  10276  ltoddhalfle  10293  halfleoddlt  10294  nn0ob  10308  flodddiv4  10334  bezoutlema  10388  bezoutlemb  10389  qredeu  10479