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

Theorem 1cnd 6841
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 6776 . 2 1
21a1i 9 1 (φ → 1 ℂ)
Colors of variables: wff set class
Syntax hints:  wi 4   wcel 1390  cc 6709  1c1 6712
This theorem was proved from axioms:  ax-1 5  ax-mp 7  ax-1cn 6776
This theorem is referenced by:  recrecap  7467  rec11ap  7468  rec11rap  7469  rerecclap  7488  recp1lt1  7646  nn1m1nn  7713  add1p1  7951  sub1m1  7952  cnm2m1cnm3  7953  peano2z  8057  zaddcllempos  8058  peano2zm  8059  zaddcllemneg  8060  nn0n0n1ge2  8087  zneo  8115  peano5uzti  8122  lincmb01cmp  8641  iccf1o  8642  zpnn0elfzo1  8834  ubmelm1fzo  8852  fzoshftral  8864  binom3  9019  zesq  9020
  Copyright terms: Public domain W3C validator