Theorem 3p1e4 11030

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

Syntax hints:   = wceq 1475  (class class class)co 6549  1c1 9816   + caddc 9818  3c3 10948  4c4 10949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-cleq 2603  df-4 10958

This theorem is referenced by:  7t6e42  11528  8t5e40  11533  8t5e40OLD  11534  9t5e45  11542  fac4  12930  4bc3eq4  12977  hash4  13056  s4len  13494  bpoly4  14629  2exp16  15635  43prm  15667  83prm  15668  317prm  15671  prmo4  15673  1259lem2  15677  1259lem3  15678  1259lem4  15679  1259lem5  15680  2503lem1  15682  2503lem2  15683  4001lem1  15686  4001lem2  15687  4001lem4  15689  4001prm  15690  sincos6thpi  24071  binom4  24377  quartlem1  24384  log2ublem3  24475  log2ub  24476  bclbnd  24805  tgcgr4  25226  4cycl4v4e  26194  4cycl4dv4e  26196  ex-opab  26681  ex-ind-dvds  26710  fib4  29793  fib5  29794  inductionexd  37473  lhe4.4ex1a  37550  stoweidlem26  38919  stoweidlem34  38927  smfmullem2  39677  fmtno5lem4  40006  fmtno5  40007  fmtno5faclem2  40030  3ndvds4  40048  139prmALT  40049  31prm  40050  m5prm  40051  sgoldbalt  40203  nnsum3primesle9  40210  nnsum4primeseven  40216  nnsum4primesevenALTV  40217  upgr4cycl4dv4e  41352