Theorem 1p1e2 8861

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 8803	. 2 |- 2 = ( 1 + 1 )
2	1	eqcomi 2144	1 |- ( 1 + 1 ) = 2

Syntax hints:   = wceq 1332  (class class class)co 5782   1c1 7645   + caddc 7647   2c2 8795

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 1424  ax-gen 1426  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-cleq 2133  df-2 8803

This theorem is referenced by:  2m1e1  8862  add1p1  8993  sub1m1  8994  nn0n0n1ge2  9145  3halfnz  9172  10p10e20  9300  5t4e20  9307  6t4e24  9311  7t3e21  9315  8t3e24  9321  9t3e27  9328  fldiv4p1lem1div2  10109  m1modge3gt1  10175  fac2  10509  hash2  10590  nn0o1gt2  11638  3lcm2e6woprm  11803  logbleb  13086  logblt  13087  ex-exp  13110