Theorem 1p1e2 8155

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

Syntax hints:   = wceq 1284  (class class class)co 5532   1c1 6982   + caddc 6984   2c2 8089

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 1376  ax-gen 1378  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-cleq 2074  df-2 8098

This theorem is referenced by:  2m1e1  8156  add1p1  8280  sub1m1  8281  nn0n0n1ge2  8418  3halfnz  8444  10p10e20  8571  5t4e20  8578  6t4e24  8582  7t3e21  8586  8t3e24  8592  9t3e27  8599  fldiv4p1lem1div2  9307  m1modge3gt1  9373  fac2  9658  nn0o1gt2  10305  3lcm2e6woprm  10468