Theorem 2p1e3 9124

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

Syntax hints:   = wceq 1364  (class class class)co 5922  1c1 7880   + caddc 7882  2c2 9041  3c3 9042

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 9050

This theorem is referenced by:  1p2e3  9125  cnm2m1cnm3  9243  6t5e30  9563  7t5e35  9568  8t4e32  9573  9t4e36  9580  decbin3  9598  halfthird  9599  fz0to3un2pr  10198  m1modge3gt1  10463  fac3  10824  hash3  10905  nn0o1gt2  12070  flodddiv4  12101  3exp3  12607  2lgsoddprmlem3c  15350