Theorem 2p1e3 9255

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 9181	. 2 ⊢ 3 = (2 + 1)
2	1	eqcomi 2233	1 ⊢ (2 + 1) = 3

Syntax hints:   = wceq 1395  (class class class)co 6007  1c1 8011   + caddc 8013  2c2 9172  3c3 9173

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 9181

This theorem is referenced by:  1p2e3  9256  cnm2m1cnm3  9374  6t5e30  9695  7t5e35  9700  8t4e32  9705  9t4e36  9712  decbin3  9730  halfthird  9731  fz0to3un2pr  10331  m1modge3gt1  10605  fac3  10966  hash3  11048  nn0o1gt2  12431  flodddiv4  12462  3exp3  12976  2lgsoddprmlem3c  15803