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

Theorem 1p1e2 9153
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 9095 . 2 2 = (1 + 1)
21eqcomi 2209 1 (1 + 1) = 2
Colors of variables: wff set class
Syntax hints:   = wceq 1373  (class class class)co 5944  1c1 7926   + caddc 7928  2c2 9087
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 1470  ax-gen 1472  ax-ext 2187
This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-2 9095
This theorem is referenced by:  2m1e1  9154  add1p1  9287  sub1m1  9288  nn0n0n1ge2  9443  3halfnz  9470  10p10e20  9598  5t4e20  9605  6t4e24  9609  7t3e21  9613  8t3e24  9619  9t3e27  9626  fz0to3un2pr  10245  fldiv4p1lem1div2  10448  m1modge3gt1  10516  fac2  10876  hash2  10957  nn0o1gt2  12216  3lcm2e6woprm  12408  2exp8  12758  2exp11  12759  2exp16  12760  logbleb  15433  logblt  15434  1sgm2ppw  15467  ex-exp  15663
  Copyright terms: Public domain W3C validator