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

Theorem 1cnd 7024
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 6958 . 2 1 ∈ ℂ
21a1i 9 1 (𝜑 → 1 ∈ ℂ)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1393  cc 6868  1c1 6871
This theorem was proved from axioms:  ax-1 5  ax-mp 7  ax-1cn 6958
This theorem is referenced by:  recrecap  7661  rec11ap  7662  rec11rap  7663  rerecclap  7682  recp1lt1  7841  nn1m1nn  7908  add1p1  8147  sub1m1  8148  cnm2m1cnm3  8149  peano2z  8253  zaddcllempos  8254  peano2zm  8255  zaddcllemneg  8256  nn0n0n1ge2  8283  zneo  8311  peano5uzti  8318  lincmb01cmp  8838  iccf1o  8839  zpnn0elfzo1  9031  ubmelm1fzo  9049  fzoshftral  9061  binom3  9244  zesq  9245  resqrexlemover  9486  absexpzap  9554
  Copyright terms: Public domain W3C validator