Theorem 1p1e2 8837

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

Syntax hints:   = wceq 1331  (class class class)co 5774  1c1 7621   + caddc 7623  2c2 8771

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 1423  ax-gen 1425  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-2 8779

This theorem is referenced by:  2m1e1  8838  add1p1  8969  sub1m1  8970  nn0n0n1ge2  9121  3halfnz  9148  10p10e20  9276  5t4e20  9283  6t4e24  9287  7t3e21  9291  8t3e24  9297  9t3e27  9304  fldiv4p1lem1div2  10078  m1modge3gt1  10144  fac2  10477  hash2  10558  nn0o1gt2  11602  3lcm2e6woprm  11767  ex-exp  12939