Theorem 1p1e2 9354

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

Syntax hints:   = wceq 1398  (class class class)co 6050   1c1 8128   + caddc 8130   2c2 9288

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 2214

This theorem depends on definitions:  df-bi 117  df-cleq 2225  df-2 9296

This theorem is referenced by:  2m1e1  9355  add1p1  9488  sub1m1  9489  nn0n0n1ge2  9648  3halfnz  9675  10p10e20  9803  5t4e20  9810  6t4e24  9814  7t3e21  9818  8t3e24  9824  9t3e27  9831  fz0to3un2pr  10457  fldiv4p1lem1div2  10665  m1modge3gt1  10733  fac2  11093  hash2  11177  s2leng  11481  nn0o1gt2  12591  3lcm2e6woprm  12783  2exp8  13133  2exp11  13134  2exp16  13135  ballotfilem2  13142  logbleb  15826  logblt  15827  1sgm2ppw  15863  1loopgrvd2fi  16300  2wlklem  16371  clwwlkext2edg  16417  konigsberglem1  16483  konigsberglem2  16484  konigsberglem3  16485  ex-exp  16495