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

Theorem 1cnd 6801
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 6736 . 2 1
21a1i 9 1 (φ → 1 ℂ)
Colors of variables: wff set class
Syntax hints:  wi 4   wcel 1390  cc 6669  1c1 6672
This theorem was proved from axioms:  ax-1 5  ax-mp 7  ax-1cn 6736
This theorem is referenced by:  recrecap  7427  rec11ap  7428  rec11rap  7429  rerecclap  7448  recp1lt1  7606  nn1m1nn  7673  add1p1  7911  sub1m1  7912  cnm2m1cnm3  7913  peano2z  8017  zaddcllempos  8018  peano2zm  8019  zaddcllemneg  8020  nn0n0n1ge2  8047  zneo  8075  peano5uzti  8082  lincmb01cmp  8601  iccf1o  8602  zpnn0elfzo1  8794  ubmelm1fzo  8812  fzoshftral  8824  binom3  8979  zesq  8980
  Copyright terms: Public domain W3C validator