Theorem 2p1e3 9438

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

This proof depends on syntax axioms:   = wceq 1402  (class class class)co 6085   1c1 8180   + caddc 8182   2c2 9355   3c3 9356

This proof depends on 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 proof depends on definitions:  df-bi 117  df-cleq 2231  df-3 9364

This theorem is used by:  1p2e3  9439  cnm2m1cnm3  9557  6t5e30  9883  7t5e35  9888  8t4e32  9893  9t4e36  9900  decbin3  9918  halfthird  9919  fz0to3un2pr  10530  m1modge3gt1  10808  fac3  11170  hash3  11254  hashtpgim  11297  nn0o1gt2  12672  flodddiv4  12703  3exp3  13217  log2ublem3  16085  log2ublog2  16086  birthdaylog2  16090  2lgsoddprmlem3c  16228  clwwlknonex2lem1  16678  clwwlknonex2lem2  16679  konigsberglem1  16729  konigsberglem2  16730  konigsberglem3  16731