Theorem 1p1e2 9238

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

Syntax hints:   = wceq 1395  (class class class)co 6007   1c1 8011   + caddc 8013   2c2 9172

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 1493  ax-gen 1495  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-2 9180

This theorem is referenced by:  2m1e1  9239  add1p1  9372  sub1m1  9373  nn0n0n1ge2  9528  3halfnz  9555  10p10e20  9683  5t4e20  9690  6t4e24  9694  7t3e21  9698  8t3e24  9704  9t3e27  9711  fz0to3un2pr  10331  fldiv4p1lem1div2  10537  m1modge3gt1  10605  fac2  10965  hash2  11047  s2leng  11337  nn0o1gt2  12432  3lcm2e6woprm  12624  2exp8  12974  2exp11  12975  2exp16  12976  logbleb  15651  logblt  15652  1sgm2ppw  15685  2wlklem  16120  clwwlkext2edg  16164  ex-exp  16174