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  9898  7t5e35  9903  8t4e32  9908  9t4e36  9915  decbin3  9933  halfthird  9934  fz0to3un2pr  10546  m1modge3gt1  10828  fac3  11191  hash3  11275  hashtpgim  11318  nn0o1gt2  12696  flodddiv4  12727  3exp3  13246  13prm  13258  37prm  13263  43prm  13264  83prm  13265  139prm  13266  163prm  13267  317prm  13268  631prm  13269  1259lem1  13270  1259lem2  13271  1259lem3  13272  1259lem4  13273  1259lem5  13274  1259prm  13275  log2ublem3  16240  log2ublog2  16241  birthdaylog2  16245  chtqub  16313  2lgsoddprmlem3c  16450  clwwlknonex2lem1  16900  clwwlknonex2lem2  16901  konigsberglem1  16951  konigsberglem2  16952  konigsberglem3  16953