Theorem 1p1e2 9371

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

Syntax hints:   = wceq 1398  (class class class)co 6058  1c1 8144   + caddc 8146  2c2 9305

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 2216

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-2 9313

This theorem is referenced by:  2m1e1  9372  add1p1  9505  sub1m1  9506  nn0n0n1ge2  9665  3halfnz  9693  10p10e20  9821  5t4e20  9828  6t4e24  9832  7t3e21  9836  8t3e24  9842  9t3e27  9849  fz0to3un2pr  10479  fldiv4p1lem1div2  10689  m1modge3gt1  10757  fac2  11118  hash2  11202  s2leng  11506  nn0o1gt2  12616  3lcm2e6woprm  12808  2exp8  13158  2exp11  13159  2exp16  13160  ballotfilem2  13172  ballotfilemfc0  13176  ballotfilemfcc  13177  logbleb  15952  logblt  15953  1sgm2ppw  15989  1loopgrvd2fi  16426  2wlklem  16497  clwwlkext2edg  16543  konigsberglem1  16609  konigsberglem2  16610  konigsberglem3  16611  ex-exp  16621