Theorem 2p1e3 9276

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

Syntax hints:   = wceq 1397  (class class class)co 6017  1c1 8032   + caddc 8034  2c2 9193  3c3 9194

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 1495  ax-gen 1497  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-3 9202

This theorem is referenced by:  1p2e3  9277  cnm2m1cnm3  9395  6t5e30  9716  7t5e35  9721  8t4e32  9726  9t4e36  9733  decbin3  9751  halfthird  9752  fz0to3un2pr  10357  m1modge3gt1  10632  fac3  10993  hash3  11076  nn0o1gt2  12465  flodddiv4  12496  3exp3  13010  2lgsoddprmlem3c  15837  clwwlknonex2lem1  16287  clwwlknonex2lem2  16288