Theorem 2p1e3 9267

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

Syntax hints:   = wceq 1395  (class class class)co 6013  1c1 8023   + caddc 8025  2c2 9184  3c3 9185

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 1493  ax-gen 1495  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-3 9193

This theorem is referenced by:  1p2e3  9268  cnm2m1cnm3  9386  6t5e30  9707  7t5e35  9712  8t4e32  9717  9t4e36  9724  decbin3  9742  halfthird  9743  fz0to3un2pr  10348  m1modge3gt1  10623  fac3  10984  hash3  11067  nn0o1gt2  12456  flodddiv4  12487  3exp3  13001  2lgsoddprmlem3c  15828  clwwlknonex2lem1  16232  clwwlknonex2lem2  16233