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

Theorem 1p1e2 8274
Description: 1 + 1 = 2. (Contributed by NM, 1-Apr-2008.)
Assertion
Ref Expression
1p1e2 (1 + 1) = 2

Proof of Theorem 1p1e2
StepHypRef Expression
1 df-2 8217 . 2 2 = (1 + 1)
21eqcomi 2087 1 (1 + 1) = 2
Colors of variables: wff set class
Syntax hints:   = wceq 1285  (class class class)co 5563  1c1 7096   + caddc 7098  2c2 8208
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-ext 2065
This theorem depends on definitions:  df-bi 115  df-cleq 2076  df-2 8217
This theorem is referenced by:  2m1e1  8275  add1p1  8399  sub1m1  8400  nn0n0n1ge2  8551  3halfnz  8577  10p10e20  8704  5t4e20  8711  6t4e24  8715  7t3e21  8719  8t3e24  8725  9t3e27  8732  fldiv4p1lem1div2  9439  m1modge3gt1  9505  fac2  9807  hash2  9888  nn0o1gt2  10512  3lcm2e6woprm  10675
  Copyright terms: Public domain W3C validator