Theorem 1p1e2 9152

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

Syntax hints:   = wceq 1372  (class class class)co 5943  1c1 7925   + caddc 7927  2c2 9086

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 1469  ax-gen 1471  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-cleq 2197  df-2 9094

This theorem is referenced by:  2m1e1  9153  add1p1  9286  sub1m1  9287  nn0n0n1ge2  9442  3halfnz  9469  10p10e20  9597  5t4e20  9604  6t4e24  9608  7t3e21  9612  8t3e24  9618  9t3e27  9625  fz0to3un2pr  10244  fldiv4p1lem1div2  10446  m1modge3gt1  10514  fac2  10874  hash2  10955  nn0o1gt2  12187  3lcm2e6woprm  12379  2exp8  12729  2exp11  12730  2exp16  12731  logbleb  15404  logblt  15405  1sgm2ppw  15438  ex-exp  15625