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  10822  fac3  11185  hash3  11269  hashtpgim  11312  nn0o1gt2  12690  flodddiv4  12721  3exp3  13240  13prm  13252  37prm  13257  43prm  13258  83prm  13259  139prm  13260  163prm  13261  317prm  13262  631prm  13263  1259lem1  13264  1259lem2  13265  1259lem3  13266  1259lem4  13267  1259lem5  13268  1259prm  13269  log2ublem3  16145  log2ublog2  16146  birthdaylog2  16150  chtqub  16218  2lgsoddprmlem3c  16350  clwwlknonex2lem1  16800  clwwlknonex2lem2  16801  konigsberglem1  16851  konigsberglem2  16852  konigsberglem3  16853