Theorem 1p1e2 9050

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

Syntax hints:   = wceq 1363  (class class class)co 5888   1c1 7826   + caddc 7828   2c2 8984

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1457  ax-gen 1459  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-cleq 2180  df-2 8992

This theorem is referenced by:  2m1e1  9051  add1p1  9182  sub1m1  9183  nn0n0n1ge2  9337  3halfnz  9364  10p10e20  9492  5t4e20  9499  6t4e24  9503  7t3e21  9507  8t3e24  9513  9t3e27  9520  fz0to3un2pr  10137  fldiv4p1lem1div2  10319  m1modge3gt1  10385  fac2  10725  hash2  10806  nn0o1gt2  11924  3lcm2e6woprm  12100  logbleb  14732  logblt  14733  ex-exp  14832