Theorem 3p1e4 12390

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

Syntax hints:   = wceq 1533  (class class class)co 7419  1c1 11141   + caddc 11143  3c3 12301  4c4 12302

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-cleq 2717  df-4 12310

This theorem is referenced by:  7t6e42  12823  8t5e40  12828  9t5e45  12835  fac4  14276  hash4  14402  s4len  14886  bpoly4  16039  2exp16  17063  43prm  17094  83prm  17095  317prm  17098  1259lem2  17104  1259lem3  17105  1259lem4  17106  1259lem5  17107  2503lem1  17109  2503lem2  17110  4001lem1  17113  4001lem2  17114  4001lem4  17116  4001prm  17117  binom4  26827  quartlem1  26834  log2ublem3  26925  log2ub  26926  bclbnd  27258  addsqnreup  27421  tgcgr4  28407  upgr4cycl4dv4e  30067  ex-opab  30314  ex-ind-dvds  30343  fib4  34155  fib5  34156  hgt750lem  34414  hgt750lem2  34415  3lexlogpow5ineq1  41657  3lexlogpow5ineq5  41663  aks4d1p1p5  41678  aks4d1p1  41679  235t711  42002  3cubeslem3l  42248  3cubeslem3r  42249  inductionexd  43727  lhe4.4ex1a  43908  stoweidlem26  45552  stoweidlem34  45560  smfmullem2  46318  fmtno5lem4  47033  fmtno5  47034  fmtno5faclem2  47057  3ndvds4  47072  139prmALT  47073  31prm  47074  m5prm  47075  11t31e341  47209  2exp340mod341  47210  8exp8mod9  47213  sbgoldbalt  47258  sbgoldbo  47264  nnsum3primesle9  47271  nnsum4primeseven  47277  nnsum4primesevenALTV  47278  ackval3  47942  ackval3012  47951  ackval41a  47953  ackval41  47954  ackval42  47955