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

Theorem 0p1e1 8858
Description: 0 + 1 = 1. (Contributed by David A. Wheeler, 7-Jul-2016.)
Assertion
Ref Expression
0p1e1 (0 + 1) = 1

Proof of Theorem 0p1e1
StepHypRef Expression
1 ax-1cn 7737 . 2 1 ∈ ℂ
21addid2i 7929 1 (0 + 1) = 1
Colors of variables: wff set class
Syntax hints:   = wceq 1332  (class class class)co 5782  0cc0 7644  1c1 7645   + caddc 7647
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515  ax-ext 2122  ax-1cn 7737  ax-icn 7739  ax-addcl 7740  ax-mulcl 7742  ax-addcom 7744  ax-i2m1 7749  ax-0id 7752
This theorem depends on definitions:  df-bi 116  df-cleq 2133  df-clel 2136
This theorem is referenced by:  fv0p1e1  8859  zgt0ge1  9136  nn0lt10b  9155  gtndiv  9170  nn0ind-raph  9192  1e0p1  9247  fz01en  9864  fz01or  9922  fz0tp  9932  elfzonlteqm1  10018  fzo0to2pr  10026  fzo0to3tp  10027  fldiv4p1lem1div2  10109  mulp1mod1  10169  1tonninf  10244  expp1  10331  facp1  10508  faclbnd  10519  bcm1k  10538  bcval5  10541  bcpasc  10544  hash1  10589  binomlem  11284  isumnn0nn  11294  ege2le3  11414  ef4p  11437  eirraplem  11519  nn0o1gt2  11638  pw2dvdslemn  11879  ennnfonelemjn  11951  exmidunben  11975  012of  13363  2o01f  13364  isomninnlem  13400  iswomninnlem  13417  ismkvnnlem  13419
  Copyright terms: Public domain W3C validator