Theorem 3p1e4 9449

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 9374	. 2 ⊢ 4 = (3 + 1)
2	1	eqcomi 2242	1 ⊢ (3 + 1) = 4

This proof depends on syntax axioms:   = wceq 1402  (class class class)co 6088  1c1 8186   + caddc 8188  3c3 9365  4c4 9366

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 9374

This theorem is used by:  7t6e42  9904  8t5e40  9909  9t5e45  9916  fac4  11192  4bc3eq4  11233  hash4  11276  2exp16  13245  43prm  13264  83prm  13265  317prm  13268  1259lem2  13271  1259lem3  13272  1259lem4  13273  1259lem5  13274  cosq23lt0  16077  binom4  16236  log2ublem3  16240  log2ublog2  16241  bclbnd  16324