Theorem 1p1e2 8970

Description: 1 + 1 = 2. (Contributed by NM, 1-Apr-2008.)

Assertion

Ref	Expression
1p1e2	⊢ (1 + 1) = 2

Proof of Theorem 1p1e2

Step	Hyp	Ref	Expression
1		df-2 8912	. 2 ⊢ 2 = (1 + 1)
2	1	eqcomi 2169	1 ⊢ (1 + 1) = 2

Syntax hints:   = wceq 1343  (class class class)co 5841  1c1 7750   + caddc 7752  2c2 8904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158  df-2 8912

This theorem is referenced by:  2m1e1  8971  add1p1  9102  sub1m1  9103  nn0n0n1ge2  9257  3halfnz  9284  10p10e20  9412  5t4e20  9419  6t4e24  9423  7t3e21  9427  8t3e24  9433  9t3e27  9440  fz0to3un2pr  10054  fldiv4p1lem1div2  10236  m1modge3gt1  10302  fac2  10640  hash2  10721  nn0o1gt2  11838  3lcm2e6woprm  12014  logbleb  13479  logblt  13480  ex-exp  13568