Theorem 1p1e2 9430

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

This proof depends on syntax axioms:   = wceq 1402  (class class class)co 6088   1c1 8186   + caddc 8188   2c2 9364

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 9372

This theorem is used by:  2m1e1  9431  add1p1  9566  sub1m1  9567  nn0n0n1ge2  9726  3halfnz  9754  10p10e20  9887  5t4e20  9894  6t4e24  9898  7t3e21  9902  8t3e24  9908  9t3e27  9915  fz0to3un2pr  10547  fldiv4p1lem1div2  10761  m1modge3gt1  10829  fac2  11191  hash2  11275  s2leng  11583  nn0o1gt2  12697  3lcm2e6woprm  12889  2exp8  13244  2exp11  13245  2exp16  13246  prmlem0  13249  prmlem2  13263  37prm  13264  43prm  13265  83prm  13266  317prm  13269  631prm  13270  1259lem1  13271  1259lem2  13272  1259lem4  13274  1259lem5  13275  ballotfilem2  13286  ballotfilemfc0  13290  ballotfilemfcc  13291  logfac  16126  logbleb  16197  logblt  16198  log2ublem3  16223  log2ublog2  16224  1sgm2ppw  16289  1loopgrvd2fi  16751  2wlklem  16822  clwwlkext2edg  16868  konigsberglem1  16934  konigsberglem2  16935  konigsberglem3  16936  ex-exp  16946