Theorem 1p1e2 8222

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

Syntax hints:   = wceq 1285  (class class class)co 5543   1c1 7044   + caddc 7046   2c2 8156

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ext 2064

This theorem depends on definitions:  df-bi 115  df-cleq 2075  df-2 8165

This theorem is referenced by:  2m1e1  8223  add1p1  8347  sub1m1  8348  nn0n0n1ge2  8499  3halfnz  8525  10p10e20  8652  5t4e20  8659  6t4e24  8663  7t3e21  8667  8t3e24  8673  9t3e27  8680  fldiv4p1lem1div2  9387  m1modge3gt1  9453  fac2  9755  size2  9836  nn0o1gt2  10449  3lcm2e6woprm  10612