Theorem 3p1e4 9443

Description: 3 + 1 = 4. (Contributed by Mario Carneiro, 18-Apr-2015.)

Assertion

Ref	Expression
3p1e4	⊢ (3 + 1) = 4

Proof of Theorem 3p1e4

Step	Hyp	Ref	Expression
1		df-4 9368	. 2 ⊢ 4 = (3 + 1)
2	1	eqcomi 2242	1 ⊢ (3 + 1) = 4

This proof depends on syntax axioms:   = wceq 1402  (class class class)co 6085  1c1 8181   + caddc 8183  3c3 9359  4c4 9360

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-4 9368

This theorem is used by:  7t6e42  9899  8t5e40  9904  9t5e45  9911  fac4  11187  4bc3eq4  11228  hash4  11271  2exp16  13240  43prm  13259  83prm  13260  317prm  13263  1259lem2  13266  1259lem3  13267  1259lem4  13268  1259lem5  13269  cosq23lt0  16026  binom4  16180  log2ublem3  16184  log2ublog2  16185  bclbnd  16268