Theorem 2p1e3 9240

Description: 2 + 1 = 3. (Contributed by Mario Carneiro, 18-Apr-2015.)

Assertion

Ref	Expression
2p1e3	⊢ (2 + 1) = 3

Proof of Theorem 2p1e3

Step	Hyp	Ref	Expression
1		df-3 9166	. 2 ⊢ 3 = (2 + 1)
2	1	eqcomi 2233	1 ⊢ (2 + 1) = 3

Syntax hints:   = wceq 1395  (class class class)co 6000  1c1 7996   + caddc 7998  2c2 9157  3c3 9158

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 1493  ax-gen 1495  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-3 9166

This theorem is referenced by:  1p2e3  9241  cnm2m1cnm3  9359  6t5e30  9680  7t5e35  9685  8t4e32  9690  9t4e36  9697  decbin3  9715  halfthird  9716  fz0to3un2pr  10315  m1modge3gt1  10588  fac3  10949  hash3  11030  nn0o1gt2  12411  flodddiv4  12442  3exp3  12956  2lgsoddprmlem3c  15782