Theorem 3p1e4 12354

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

Syntax hints:   = wceq 1542  (class class class)co 7406  1c1 11108   + caddc 11110  3c3 12265  4c4 12266

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-4 12274

This theorem is referenced by:  7t6e42  12787  8t5e40  12792  9t5e45  12799  fac4  14238  hash4  14364  s4len  14847  bpoly4  16000  2exp16  17021  43prm  17052  83prm  17053  317prm  17056  1259lem2  17062  1259lem3  17063  1259lem4  17064  1259lem5  17065  2503lem1  17067  2503lem2  17068  4001lem1  17071  4001lem2  17072  4001lem4  17074  4001prm  17075  binom4  26345  quartlem1  26352  log2ublem3  26443  log2ub  26444  bclbnd  26773  addsqnreup  26936  tgcgr4  27772  upgr4cycl4dv4e  29428  ex-opab  29675  ex-ind-dvds  29704  fib4  33392  fib5  33393  hgt750lem  33652  hgt750lem2  33653  3lexlogpow5ineq1  40908  3lexlogpow5ineq5  40914  aks4d1p1p5  40929  aks4d1p1  40930  235t711  41201  3cubeslem3l  41410  3cubeslem3r  41411  inductionexd  42892  lhe4.4ex1a  43074  stoweidlem26  44729  stoweidlem34  44737  smfmullem2  45495  fmtno5lem4  46211  fmtno5  46212  fmtno5faclem2  46235  3ndvds4  46250  139prmALT  46251  31prm  46252  m5prm  46253  11t31e341  46387  2exp340mod341  46388  8exp8mod9  46391  sbgoldbalt  46436  sbgoldbo  46442  nnsum3primesle9  46449  nnsum4primeseven  46455  nnsum4primesevenALTV  46456  ackval3  47323  ackval3012  47332  ackval41a  47334  ackval41  47335  ackval42  47336