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  9905  8t5e40  9910  9t5e45  9917  fac4  11193  4bc3eq4  11234  hash4  11277  2exp16  13246  43prm  13265  83prm  13266  317prm  13269  1259lem2  13272  1259lem3  13273  1259lem4  13274  1259lem5  13275  cosq23lt0  16060  binom4  16219  log2ublem3  16223  log2ublog2  16224  bclbnd  16307