Theorem 1p1e2 9400

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 9342	. 2 ⊢ 2 = (1 + 1)
2	1	eqcomi 2242	1 ⊢ (1 + 1) = 2

Syntax hints:   = wceq 1402  (class class class)co 6075  1c1 8170   + caddc 8172  2c2 9334

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 1500  ax-gen 1502  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-cleq 2231  df-2 9342

This theorem is referenced by:  2m1e1  9401  add1p1  9534  sub1m1  9535  nn0n0n1ge2  9694  3halfnz  9722  10p10e20  9850  5t4e20  9857  6t4e24  9861  7t3e21  9865  8t3e24  9871  9t3e27  9878  fz0to3un2pr  10508  fldiv4p1lem1div2  10718  m1modge3gt1  10786  fac2  11147  hash2  11231  s2leng  11539  nn0o1gt2  12650  3lcm2e6woprm  12842  2exp8  13192  2exp11  13193  2exp16  13194  ballotfilem2  13206  ballotfilemfc0  13210  ballotfilemfcc  13211  logfac  15918  logbleb  15986  logblt  15987  1sgm2ppw  16023  1loopgrvd2fi  16460  2wlklem  16531  clwwlkext2edg  16577  konigsberglem1  16643  konigsberglem2  16644  konigsberglem3  16645  ex-exp  16655