Theorem 3p1e4 9442

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 9367	. 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 8180   + caddc 8182  3c3 9358  4c4 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-4 9367

This theorem is used by:  7t6e42  9898  8t5e40  9903  9t5e45  9910  fac4  11185  4bc3eq4  11226  hash4  11269  2exp16  13237  43prm  13256  83prm  13257  317prm  13260  1259lem2  13263  1259lem3  13264  1259lem4  13265  1259lem5  13266  cosq23lt0  15984  binom4  16138  log2ublem3  16142  log2ublog2  16143  bclbnd  16205