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

Theorem 0p1e1 8104
 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 7035 . 2 1 ∈ ℂ
21addid2i 7217 1 (0 + 1) = 1
 Colors of variables: wff set class Syntax hints:   = wceq 1259  (class class class)co 5540  0cc0 6947  1c1 6948   + caddc 6950 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416  ax-17 1435  ax-ial 1443  ax-ext 2038  ax-1cn 7035  ax-icn 7037  ax-addcl 7038  ax-mulcl 7040  ax-addcom 7042  ax-i2m1 7047  ax-0id 7050 This theorem depends on definitions:  df-bi 114  df-cleq 2049  df-clel 2052 This theorem is referenced by:  zgt0ge1  8360  nn0lt10b  8379  gtndiv  8393  nn0ind-raph  8414  1e0p1  8468  fz01en  9019  fz0tp  9083  elfzonlteqm1  9168  fzo0to2pr  9176  fzo0to3tp  9177  fldiv4p1lem1div2  9255  mulp1mod1  9315  expp1  9427  facp1  9598  faclbnd  9609  bcm1k  9628  ibcval5  9631  bcpasc  9634  fz01or  10190  nn0o1gt2  10217  pw2dvdslemn  10253
 Copyright terms: Public domain W3C validator