Theorem 1p1e2 8830

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

Syntax hints:   = wceq 1331  (class class class)co 5767   1c1 7614   + caddc 7616   2c2 8764

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 2119

This theorem depends on definitions:  df-bi 116  df-cleq 2130  df-2 8772

This theorem is referenced by:  2m1e1  8831  add1p1  8962  sub1m1  8963  nn0n0n1ge2  9114  3halfnz  9141  10p10e20  9269  5t4e20  9276  6t4e24  9280  7t3e21  9284  8t3e24  9290  9t3e27  9297  fldiv4p1lem1div2  10071  m1modge3gt1  10137  fac2  10470  hash2  10551  nn0o1gt2  11591  3lcm2e6woprm  11756  ex-exp  12928