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

Theorem 1p1e2 8222
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 8165 . 2  |-  2  =  ( 1  +  1 )
21eqcomi 2086 1  |-  ( 1  +  1 )  =  2
Colors of variables: wff set class
Syntax hints:    = wceq 1285  (class class class)co 5543   1c1 7044    + caddc 7046   2c2 8156
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 2064
This theorem depends on definitions:  df-bi 115  df-cleq 2075  df-2 8165
This theorem is referenced by:  2m1e1  8223  add1p1  8347  sub1m1  8348  nn0n0n1ge2  8499  3halfnz  8525  10p10e20  8652  5t4e20  8659  6t4e24  8663  7t3e21  8667  8t3e24  8673  9t3e27  8680  fldiv4p1lem1div2  9387  m1modge3gt1  9453  fac2  9755  size2  9836  nn0o1gt2  10449  3lcm2e6woprm  10612
  Copyright terms: Public domain W3C validator