Theorem 2p1e3 9371

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

Syntax hints:   = wceq 1398  (class class class)co 6050  1c1 8128   + caddc 8130  2c2 9288  3c3 9289

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 2214

This theorem depends on definitions:  df-bi 117  df-cleq 2225  df-3 9297

This theorem is referenced by:  1p2e3  9372  cnm2m1cnm3  9490  6t5e30  9815  7t5e35  9820  8t4e32  9825  9t4e36  9832  decbin3  9850  halfthird  9851  fz0to3un2pr  10457  m1modge3gt1  10733  fac3  11094  hash3  11178  hashtpgim  11217  nn0o1gt2  12591  flodddiv4  12622  3exp3  13136  2lgsoddprmlem3c  15982  clwwlknonex2lem1  16432  clwwlknonex2lem2  16433  konigsberglem1  16483  konigsberglem2  16484  konigsberglem3  16485