Theorem 2p1e3 9440

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 9366	. 2 |- 3 = ( 2 + 1 )
2	1	eqcomi 2242	1 |- ( 2 + 1 ) = 3

This proof depends on syntax axioms:   = wceq 1402  (class class class)co 6085   1c1 8180   + caddc 8182   2c2 9357   3c3 9358

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-3 9366

This theorem is used by:  1p2e3  9441  cnm2m1cnm3  9561  6t5e30  9892  7t5e35  9897  8t4e32  9902  9t4e36  9909  decbin3  9927  halfthird  9928  fz0to3un2pr  10540  m1modge3gt1  10821  fac3  11184  hash3  11268  hashtpgim  11311  nn0o1gt2  12688  flodddiv4  12719  3exp3  13238  13prm  13250  37prm  13255  43prm  13256  83prm  13257  139prm  13258  163prm  13259  317prm  13260  631prm  13261  1259lem1  13262  1259lem2  13263  1259lem3  13264  1259lem4  13265  1259lem5  13266  1259prm  13267  log2ublem3  16142  log2ublog2  16143  birthdaylog2  16147  2lgsoddprmlem3c  16326  clwwlknonex2lem1  16776  clwwlknonex2lem2  16777  konigsberglem1  16827  konigsberglem2  16828  konigsberglem3  16829