Theorem 1p1e2 9302

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

Syntax hints:   = wceq 1398  (class class class)co 6028   1c1 8076   + caddc 8078   2c2 9236

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 9244

This theorem is referenced by:  2m1e1  9303  add1p1  9436  sub1m1  9437  nn0n0n1ge2  9594  3halfnz  9621  10p10e20  9749  5t4e20  9756  6t4e24  9760  7t3e21  9764  8t3e24  9770  9t3e27  9777  fz0to3un2pr  10403  fldiv4p1lem1div2  10611  m1modge3gt1  10679  fac2  11039  hash2  11122  s2leng  11419  nn0o1gt2  12529  3lcm2e6woprm  12721  2exp8  13071  2exp11  13072  2exp16  13073  logbleb  15755  logblt  15756  1sgm2ppw  15792  1loopgrvd2fi  16229  2wlklem  16300  clwwlkext2edg  16346  konigsberglem1  16412  konigsberglem2  16413  konigsberglem3  16414  ex-exp  16424