Theorem 1p1e2 9319

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

Syntax hints:   = wceq 1398  (class class class)co 6028  1c1 8093   + caddc 8095  2c2 9253

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 1496  ax-gen 1498  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-2 9261

This theorem is referenced by:  2m1e1  9320  add1p1  9453  sub1m1  9454  nn0n0n1ge2  9611  3halfnz  9638  10p10e20  9766  5t4e20  9773  6t4e24  9777  7t3e21  9781  8t3e24  9787  9t3e27  9794  fz0to3un2pr  10420  fldiv4p1lem1div2  10628  m1modge3gt1  10696  fac2  11056  hash2  11139  s2leng  11436  nn0o1gt2  12546  3lcm2e6woprm  12738  2exp8  13088  2exp11  13089  2exp16  13090  logbleb  15772  logblt  15773  1sgm2ppw  15809  1loopgrvd2fi  16246  2wlklem  16317  clwwlkext2edg  16363  konigsberglem1  16429  konigsberglem2  16430  konigsberglem3  16431  ex-exp  16441