Theorem 3p1e4 11097

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

Syntax hints:   = wceq 1480  (class class class)co 6604  1c1 9881   + caddc 9883  3c3 11015  4c4 11016

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-ext 2601

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-cleq 2614  df-4 11025

This theorem is referenced by:  7t6e42  11596  8t5e40  11601  8t5e40OLD  11602  9t5e45  11610  fac4  13008  4bc3eq4  13055  hash4  13135  s4len  13580  bpoly4  14715  2exp16  15721  43prm  15753  83prm  15754  317prm  15757  prmo4  15759  1259lem2  15763  1259lem3  15764  1259lem4  15765  1259lem5  15766  2503lem1  15768  2503lem2  15769  4001lem1  15772  4001lem2  15773  4001lem4  15775  4001prm  15776  sincos6thpi  24171  binom4  24477  quartlem1  24484  log2ublem3  24575  log2ub  24576  bclbnd  24905  tgcgr4  25326  upgr4cycl4dv4e  26911  ex-opab  27143  ex-ind-dvds  27172  fib4  30247  fib5  30248  inductionexd  37935  lhe4.4ex1a  38010  stoweidlem26  39550  stoweidlem34  39558  smfmullem2  40306  fmtno5lem4  40767  fmtno5  40768  fmtno5faclem2  40791  3ndvds4  40809  139prmALT  40810  31prm  40811  m5prm  40812  sgoldbalt  40964  nnsum3primesle9  40971  nnsum4primeseven  40977  nnsum4primesevenALTV  40978