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  9724  3halfnz  9753  10p10e20  9886  5t4e20  9893  6t4e24  9897  7t3e21  9901  8t3e24  9907  9t3e27  9914  fz0to3un2pr  10546  fldiv4p1lem1div2  10760  m1modge3gt1  10828  fac2  11190  hash2  11274  s2leng  11582  nn0o1gt2  12696  3lcm2e6woprm  12888  2exp8  13243  2exp11  13244  2exp16  13245  prmlem0  13248  prmlem2  13262  37prm  13263  43prm  13264  83prm  13265  317prm  13268  631prm  13269  1259lem1  13270  1259lem2  13271  1259lem4  13273  1259lem5  13274  ballotfilem2  13285  ballotfilemfc0  13289  ballotfilemfcc  13290  logfac  16143  logbleb  16214  logblt  16215  log2ublem3  16240  log2ublog2  16241  1sgm2ppw  16306  1loopgrvd2fi  16768  2wlklem  16839  clwwlkext2edg  16885  konigsberglem1  16951  konigsberglem2  16952  konigsberglem3  16953  ex-exp  16963