Theorem 1p1e2 9423

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 9365	. 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 9357

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 9365

This theorem is used by:  2m1e1  9424  add1p1  9559  sub1m1  9560  nn0n0n1ge2  9719  3halfnz  9747  10p10e20  9880  5t4e20  9887  6t4e24  9891  7t3e21  9895  8t3e24  9901  9t3e27  9908  fz0to3un2pr  10540  fldiv4p1lem1div2  10753  m1modge3gt1  10821  fac2  11183  hash2  11267  s2leng  11575  nn0o1gt2  12688  3lcm2e6woprm  12880  2exp8  13235  2exp11  13236  2exp16  13237  prmlem0  13240  prmlem2  13254  37prm  13255  43prm  13256  83prm  13257  317prm  13260  631prm  13261  1259lem1  13262  1259lem2  13263  1259lem4  13265  1259lem5  13266  ballotfilem2  13277  ballotfilemfc0  13281  ballotfilemfcc  13282  logfac  16048  logbleb  16116  logblt  16117  log2ublem3  16142  log2ublog2  16143  1sgm2ppw  16190  1loopgrvd2fi  16644  2wlklem  16715  clwwlkext2edg  16761  konigsberglem1  16827  konigsberglem2  16828  konigsberglem3  16829  ex-exp  16839