Theorem 1p1e2 9155

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

Syntax hints:   = wceq 1373  (class class class)co 5946   1c1 7928   + caddc 7930   2c2 9089

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 1470  ax-gen 1472  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-2 9097

This theorem is referenced by:  2m1e1  9156  add1p1  9289  sub1m1  9290  nn0n0n1ge2  9445  3halfnz  9472  10p10e20  9600  5t4e20  9607  6t4e24  9611  7t3e21  9615  8t3e24  9621  9t3e27  9628  fz0to3un2pr  10247  fldiv4p1lem1div2  10450  m1modge3gt1  10518  fac2  10878  hash2  10959  nn0o1gt2  12249  3lcm2e6woprm  12441  2exp8  12791  2exp11  12792  2exp16  12793  logbleb  15466  logblt  15467  1sgm2ppw  15500  ex-exp  15700