Theorem 1p1e2 9250

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

Syntax hints:   = wceq 1395  (class class class)co 6013  1c1 8023   + caddc 8025  2c2 9184

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 9192

This theorem is referenced by:  2m1e1  9251  add1p1  9384  sub1m1  9385  nn0n0n1ge2  9540  3halfnz  9567  10p10e20  9695  5t4e20  9702  6t4e24  9706  7t3e21  9710  8t3e24  9716  9t3e27  9723  fz0to3un2pr  10348  fldiv4p1lem1div2  10555  m1modge3gt1  10623  fac2  10983  hash2  11066  s2leng  11360  nn0o1gt2  12456  3lcm2e6woprm  12648  2exp8  12998  2exp11  12999  2exp16  13000  logbleb  15675  logblt  15676  1sgm2ppw  15709  1loopgrvd2fi  16111  2wlklem  16171  clwwlkext2edg  16217  ex-exp  16259