Theorem 2p1e3 9152

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

Syntax hints:   = wceq 1372  (class class class)co 5934  1c1 7908   + caddc 7910  2c2 9069  3c3 9070

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 1469  ax-gen 1471  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-cleq 2197  df-3 9078

This theorem is referenced by:  1p2e3  9153  cnm2m1cnm3  9271  6t5e30  9592  7t5e35  9597  8t4e32  9602  9t4e36  9609  decbin3  9627  halfthird  9628  fz0to3un2pr  10227  m1modge3gt1  10497  fac3  10858  hash3  10939  nn0o1gt2  12135  flodddiv4  12166  3exp3  12680  2lgsoddprmlem3c  15504