Theorem 2p1e3 9441

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 9367	. 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 8181   + caddc 8183  2c2 9358  3c3 9359

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 9367

This theorem is used by:  1p2e3  9442  cnm2m1cnm3  9562  6t5e30  9893  7t5e35  9898  8t4e32  9903  9t4e36  9910  decbin3  9928  halfthird  9929  fz0to3un2pr  10541  m1modge3gt1  10823  fac3  11186  hash3  11270  hashtpgim  11313  nn0o1gt2  12691  flodddiv4  12722  3exp3  13241  13prm  13253  37prm  13258  43prm  13259  83prm  13260  139prm  13261  163prm  13262  317prm  13263  631prm  13264  1259lem1  13265  1259lem2  13266  1259lem3  13267  1259lem4  13268  1259lem5  13269  1259prm  13270  log2ublem3  16184  log2ublog2  16185  birthdaylog2  16189  chtqub  16257  2lgsoddprmlem3c  16394  clwwlknonex2lem1  16844  clwwlknonex2lem2  16845  konigsberglem1  16895  konigsberglem2  16896  konigsberglem3  16897