Theorem 2p1e3 9244

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

Syntax hints:   = wceq 1395  (class class class)co 6001   1c1 8000   + caddc 8002   2c2 9161   3c3 9162

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 9170

This theorem is referenced by:  1p2e3  9245  cnm2m1cnm3  9363  6t5e30  9684  7t5e35  9689  8t4e32  9694  9t4e36  9701  decbin3  9719  halfthird  9720  fz0to3un2pr  10319  m1modge3gt1  10593  fac3  10954  hash3  11035  nn0o1gt2  12416  flodddiv4  12447  3exp3  12961  2lgsoddprmlem3c  15788