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

Theorem 1p1e2 9152
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 9094 . 2 2 = (1 + 1)
21eqcomi 2208 1 (1 + 1) = 2
Colors of variables: wff set class
Syntax hints:   = wceq 1372  (class class class)co 5943  1c1 7925   + caddc 7927  2c2 9086
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1469  ax-gen 1471  ax-ext 2186
This theorem depends on definitions:  df-bi 117  df-cleq 2197  df-2 9094
This theorem is referenced by:  2m1e1  9153  add1p1  9286  sub1m1  9287  nn0n0n1ge2  9442  3halfnz  9469  10p10e20  9597  5t4e20  9604  6t4e24  9608  7t3e21  9612  8t3e24  9618  9t3e27  9625  fz0to3un2pr  10244  fldiv4p1lem1div2  10446  m1modge3gt1  10514  fac2  10874  hash2  10955  nn0o1gt2  12187  3lcm2e6woprm  12379  2exp8  12729  2exp11  12730  2exp16  12731  logbleb  15404  logblt  15405  1sgm2ppw  15438  ex-exp  15625
  Copyright terms: Public domain W3C validator