Theorem 2p1e3 9277

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

Syntax hints:   = wceq 1397  (class class class)co 6018  1c1 8033   + caddc 8035  2c2 9194  3c3 9195

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 9203

This theorem is referenced by:  1p2e3  9278  cnm2m1cnm3  9396  6t5e30  9717  7t5e35  9722  8t4e32  9727  9t4e36  9734  decbin3  9752  halfthird  9753  fz0to3un2pr  10358  m1modge3gt1  10634  fac3  10995  hash3  11078  hashtpgim  11110  nn0o1gt2  12471  flodddiv4  12502  3exp3  13016  2lgsoddprmlem3c  15844  clwwlknonex2lem1  16294  clwwlknonex2lem2  16295