Theorem 2p1e3 9388

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

Syntax hints:   = wceq 1398  (class class class)co 6058   1c1 8144   + caddc 8146   2c2 9305   3c3 9306

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 1496  ax-gen 1498  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-3 9314

This theorem is referenced by:  1p2e3  9389  cnm2m1cnm3  9507  6t5e30  9833  7t5e35  9838  8t4e32  9843  9t4e36  9850  decbin3  9868  halfthird  9869  fz0to3un2pr  10479  m1modge3gt1  10757  fac3  11119  hash3  11203  hashtpgim  11242  nn0o1gt2  12616  flodddiv4  12647  3exp3  13161  2lgsoddprmlem3c  16108  clwwlknonex2lem1  16558  clwwlknonex2lem2  16559  konigsberglem1  16609  konigsberglem2  16610  konigsberglem3  16611