Theorem 1p1e2 9153

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

Syntax hints:   = wceq 1373  (class class class)co 5944  1c1 7926   + caddc 7928  2c2 9087

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 1470  ax-gen 1472  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-2 9095

This theorem is referenced by:  2m1e1  9154  add1p1  9287  sub1m1  9288  nn0n0n1ge2  9443  3halfnz  9470  10p10e20  9598  5t4e20  9605  6t4e24  9609  7t3e21  9613  8t3e24  9619  9t3e27  9626  fz0to3un2pr  10245  fldiv4p1lem1div2  10448  m1modge3gt1  10516  fac2  10876  hash2  10957  nn0o1gt2  12216  3lcm2e6woprm  12408  2exp8  12758  2exp11  12759  2exp16  12760  logbleb  15433  logblt  15434  1sgm2ppw  15467  ex-exp  15663