Theorem 2p1e3 9143

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

Syntax hints:   = wceq 1364  (class class class)co 5925  1c1 7899   + caddc 7901  2c2 9060  3c3 9061

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 1461  ax-gen 1463  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-3 9069

This theorem is referenced by:  1p2e3  9144  cnm2m1cnm3  9262  6t5e30  9582  7t5e35  9587  8t4e32  9592  9t4e36  9599  decbin3  9617  halfthird  9618  fz0to3un2pr  10217  m1modge3gt1  10482  fac3  10843  hash3  10924  nn0o1gt2  12089  flodddiv4  12120  3exp3  12634  2lgsoddprmlem3c  15458