Theorem 1p1e2 9424

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 9366	. 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 8181   + caddc 8183  2c2 9358

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 9366

This theorem is used by:  2m1e1  9425  add1p1  9560  sub1m1  9561  nn0n0n1ge2  9720  3halfnz  9748  10p10e20  9881  5t4e20  9888  6t4e24  9892  7t3e21  9896  8t3e24  9902  9t3e27  9909  fz0to3un2pr  10541  fldiv4p1lem1div2  10755  m1modge3gt1  10823  fac2  11185  hash2  11269  s2leng  11577  nn0o1gt2  12691  3lcm2e6woprm  12883  2exp8  13238  2exp11  13239  2exp16  13240  prmlem0  13243  prmlem2  13257  37prm  13258  43prm  13259  83prm  13260  317prm  13263  631prm  13264  1259lem1  13265  1259lem2  13266  1259lem4  13268  1259lem5  13269  ballotfilem2  13280  ballotfilemfc0  13284  ballotfilemfcc  13285  logfac  16090  logbleb  16158  logblt  16159  log2ublem3  16184  log2ublog2  16185  1sgm2ppw  16250  1loopgrvd2fi  16712  2wlklem  16783  clwwlkext2edg  16829  konigsberglem1  16895  konigsberglem2  16896  konigsberglem3  16897  ex-exp  16907