Theorem 1p1e2 8995

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

Syntax hints:   = wceq 1348  (class class class)co 5853  1c1 7775   + caddc 7777  2c2 8929

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-2 8937

This theorem is referenced by:  2m1e1  8996  add1p1  9127  sub1m1  9128  nn0n0n1ge2  9282  3halfnz  9309  10p10e20  9437  5t4e20  9444  6t4e24  9448  7t3e21  9452  8t3e24  9458  9t3e27  9465  fz0to3un2pr  10079  fldiv4p1lem1div2  10261  m1modge3gt1  10327  fac2  10665  hash2  10747  nn0o1gt2  11864  3lcm2e6woprm  12040  logbleb  13673  logblt  13674  ex-exp  13762