Theorem 1p1e2 8274

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 8217	. 2 ⊢ 2 = (1 + 1)
2	1	eqcomi 2087	1 ⊢ (1 + 1) = 2

Syntax hints:   = wceq 1285  (class class class)co 5563  1c1 7096   + caddc 7098  2c2 8208

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 2065

This theorem depends on definitions:  df-bi 115  df-cleq 2076  df-2 8217

This theorem is referenced by:  2m1e1  8275  add1p1  8399  sub1m1  8400  nn0n0n1ge2  8551  3halfnz  8577  10p10e20  8704  5t4e20  8711  6t4e24  8715  7t3e21  8719  8t3e24  8725  9t3e27  8732  fldiv4p1lem1div2  9439  m1modge3gt1  9505  fac2  9807  hash2  9888  nn0o1gt2  10512  3lcm2e6woprm  10675