Theorem 2p1e3 9447

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

This proof depends on syntax axioms:   = wceq 1402  (class class class)co 6088   1c1 8186   + caddc 8188   2c2 9364   3c3 9365

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 9373

This theorem is used by:  1p2e3  9448  cnm2m1cnm3  9568  6t5e30  9899  7t5e35  9904  8t4e32  9909  9t4e36  9916  decbin3  9934  halfthird  9935  fz0to3un2pr  10547  m1modge3gt1  10829  fac3  11192  hash3  11276  hashtpgim  11319  nn0o1gt2  12697  flodddiv4  12728  3exp3  13247  13prm  13259  37prm  13264  43prm  13265  83prm  13266  139prm  13267  163prm  13268  317prm  13269  631prm  13270  1259lem1  13271  1259lem2  13272  1259lem3  13273  1259lem4  13274  1259lem5  13275  1259prm  13276  log2ublem3  16223  log2ublog2  16224  birthdaylog2  16228  chtqub  16296  2lgsoddprmlem3c  16433  clwwlknonex2lem1  16883  clwwlknonex2lem2  16884  konigsberglem1  16934  konigsberglem2  16935  konigsberglem3  16936