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

Theorem 0p1e1 8209
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 7120 . 2  |-  1  e.  CC
21addid2i 7307 1  |-  ( 0  +  1 )  =  1
Colors of variables: wff set class
Syntax hints:    = wceq 1285  (class class class)co 5537   0cc0 7032   1c1 7033    + caddc 7035
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 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-ial 1468  ax-ext 2064  ax-1cn 7120  ax-icn 7122  ax-addcl 7123  ax-mulcl 7125  ax-addcom 7127  ax-i2m1 7132  ax-0id 7135
This theorem depends on definitions:  df-bi 115  df-cleq 2075  df-clel 2078
This theorem is referenced by:  zgt0ge1  8479  nn0lt10b  8498  gtndiv  8512  nn0ind-raph  8534  1e0p1  8588  fz01en  9137  fz01or  9193  fz0tp  9201  elfzonlteqm1  9285  fzo0to2pr  9293  fzo0to3tp  9294  fldiv4p1lem1div2  9376  mulp1mod1  9436  expp1  9569  facp1  9743  faclbnd  9754  bcm1k  9773  ibcval5  9776  bcpasc  9779  size1  9824  nn0o1gt2  10438  pw2dvdslemn  10676
  Copyright terms: Public domain W3C validator