Theorem 1p1e2 9421

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

This proof depends on syntax axioms:   = wceq 1402  (class class class)co 6085   1c1 8180   + caddc 8182   2c2 9355

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-2 9363

This theorem is used by:  2m1e1  9422  add1p1  9555  sub1m1  9556  nn0n0n1ge2  9715  3halfnz  9743  10p10e20  9871  5t4e20  9878  6t4e24  9882  7t3e21  9886  8t3e24  9892  9t3e27  9899  fz0to3un2pr  10530  fldiv4p1lem1div2  10740  m1modge3gt1  10808  fac2  11169  hash2  11253  s2leng  11561  nn0o1gt2  12672  3lcm2e6woprm  12864  2exp8  13214  2exp11  13215  2exp16  13216  ballotfilem2  13228  ballotfilemfc0  13232  ballotfilemfcc  13233  logfac  15995  logbleb  16063  logblt  16064  log2ublem3  16085  log2ublog2  16086  1sgm2ppw  16109  1loopgrvd2fi  16546  2wlklem  16617  clwwlkext2edg  16663  konigsberglem1  16729  konigsberglem2  16730  konigsberglem3  16731  ex-exp  16741