ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  1cnd GIF version

Theorem 1cnd 7041
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
StepHypRef Expression
1 ax-1cn 6975 . 2 1 ∈ ℂ
21a1i 9 1 (𝜑 → 1 ∈ ℂ)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1393  cc 6885  1c1 6888
This theorem was proved from axioms:  ax-1 5  ax-mp 7  ax-1cn 6975
This theorem is referenced by:  recrecap  7683  rec11ap  7684  rec11rap  7685  rerecclap  7704  recp1lt1  7863  nn1m1nn  7930  add1p1  8172  sub1m1  8173  cnm2m1cnm3  8174  div4p1lem1div2  8175  peano2z  8279  zaddcllempos  8280  peano2zm  8281  zaddcllemneg  8282  nn0n0n1ge2  8309  zneo  8337  peano5uzti  8344  lincmb01cmp  8869  iccf1o  8870  zpnn0elfzo1  9062  ubmelm1fzo  9080  fzoshftral  9092  qbtwnzlemstep  9101  rebtwn2zlemstep  9105  qbtwnrelemcalc  9108  flqaddz  9137  2tnp1ge0ge0  9141  ceiqm1l  9151  binom3  9340  zesq  9341  resqrexlemover  9582  absexpzap  9650
  Copyright terms: Public domain W3C validator