Theorem 2p1e3 9417

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

Syntax hints:   = wceq 1402  (class class class)co 6075   1c1 8170   + caddc 8172   2c2 9334   3c3 9335

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 1500  ax-gen 1502  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-cleq 2231  df-3 9343

This theorem is referenced by:  1p2e3  9418  cnm2m1cnm3  9536  6t5e30  9862  7t5e35  9867  8t4e32  9872  9t4e36  9879  decbin3  9897  halfthird  9898  fz0to3un2pr  10508  m1modge3gt1  10786  fac3  11148  hash3  11232  hashtpgim  11275  nn0o1gt2  12650  flodddiv4  12681  3exp3  13195  2lgsoddprmlem3c  16142  clwwlknonex2lem1  16592  clwwlknonex2lem2  16593  konigsberglem1  16643  konigsberglem2  16644  konigsberglem3  16645