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

Theorem 1cnd 7101
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 7035 . 2 1 ∈ ℂ
21a1i 9 1 (𝜑 → 1 ∈ ℂ)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1409  cc 6945  1c1 6948
This theorem was proved from axioms:  ax-1 5  ax-mp 7  ax-1cn 7035
This theorem is referenced by:  adddirp1d  7111  muladd11r  7230  recrecap  7760  rec11ap  7761  rec11rap  7762  rerecclap  7781  recp1lt1  7940  nn1m1nn  8008  add1p1  8231  sub1m1  8232  cnm2m1cnm3  8233  xp1d2m1eqxm1d2  8234  div4p1lem1div2  8235  peano2z  8338  zaddcllempos  8339  peano2zm  8340  zaddcllemneg  8341  nn0n0n1ge2  8369  zneo  8398  peano5uzti  8405  lincmb01cmp  8972  iccf1o  8973  zpnn0elfzo1  9166  ubmelm1fzo  9184  fzoshftral  9196  qbtwnzlemstep  9205  rebtwn2zlemstep  9209  qbtwnrelemcalc  9212  flqaddz  9247  2tnp1ge0ge0  9251  ceiqm1l  9261  qnegmod  9319  addmodlteq  9348  binom3  9534  zesq  9535  sqoddm1div8  9569  nn0opthlem1d  9588  bcm1k  9628  bcp1n  9629  bcp1m1  9633  bcpasc  9634  bcn2m1  9637  resqrexlemover  9837  absexpzap  9907  zeo3  10179  oddm1even  10186  oddp1even  10187  oexpneg  10188  ltoddhalfle  10205  halfleoddlt  10206  nn0ob  10220  flodddiv4  10246
  Copyright terms: Public domain W3C validator