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

Theorem 0p1e1 8507
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 7417 . 2 1 ∈ ℂ
21addid2i 7604 1 (0 + 1) = 1
Colors of variables: wff set class
Syntax hints:   = wceq 1289  (class class class)co 5634  0cc0 7329  1c1 7330   + caddc 7332
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-17 1464  ax-ial 1472  ax-ext 2070  ax-1cn 7417  ax-icn 7419  ax-addcl 7420  ax-mulcl 7422  ax-addcom 7424  ax-i2m1 7429  ax-0id 7432
This theorem depends on definitions:  df-bi 115  df-cleq 2081  df-clel 2084
This theorem is referenced by:  zgt0ge1  8778  nn0lt10b  8797  gtndiv  8811  nn0ind-raph  8833  1e0p1  8887  fz01en  9436  fz01or  9492  fz0tp  9500  elfzonlteqm1  9586  fzo0to2pr  9594  fzo0to3tp  9595  fldiv4p1lem1div2  9677  mulp1mod1  9737  1tonninf  9811  expp1  9927  facp1  10103  faclbnd  10114  bcm1k  10133  ibcval5  10136  bcpasc  10139  hash1  10184  binomlem  10839  isumnn0nn  10849  nn0o1gt2  10998  pw2dvdslemn  11236
  Copyright terms: Public domain W3C validator