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

Theorem 1p1e2 8509
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 8452 . 2  |-  2  =  ( 1  +  1 )
21eqcomi 2092 1  |-  ( 1  +  1 )  =  2
Colors of variables: wff set class
Syntax hints:    = wceq 1289  (class class class)co 5634   1c1 7330    + caddc 7332   2c2 8444
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-ext 2070
This theorem depends on definitions:  df-bi 115  df-cleq 2081  df-2 8452
This theorem is referenced by:  2m1e1  8510  add1p1  8635  sub1m1  8636  nn0n0n1ge2  8787  3halfnz  8813  10p10e20  8940  5t4e20  8947  6t4e24  8951  7t3e21  8955  8t3e24  8961  9t3e27  8968  fldiv4p1lem1div2  9677  m1modge3gt1  9743  fac2  10104  hash2  10185  nn0o1gt2  10998  3lcm2e6woprm  11161  ex-exp  11311
  Copyright terms: Public domain W3C validator