Theorem 3p1e4 11783

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

Syntax hints:   = wceq 1537  (class class class)co 7156  1c1 10538   + caddc 10540  3c3 11694  4c4 11695

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814  df-4 11703

This theorem is referenced by:  7t6e42  12212  8t5e40  12217  9t5e45  12224  fac4  13642  hash4  13769  s4len  14261  bpoly4  15413  2exp16  16424  43prm  16455  83prm  16456  317prm  16459  1259lem2  16465  1259lem3  16466  1259lem4  16467  1259lem5  16468  2503lem1  16470  2503lem2  16471  4001lem1  16474  4001lem2  16475  4001lem4  16477  4001prm  16478  binom4  25428  quartlem1  25435  log2ublem3  25526  log2ub  25527  bclbnd  25856  addsqnreup  26019  tgcgr4  26317  upgr4cycl4dv4e  27964  ex-opab  28211  ex-ind-dvds  28240  fib4  31662  fib5  31663  hgt750lem  31922  hgt750lem2  31923  235t711  39197  3cubeslem3l  39303  3cubeslem3r  39304  inductionexd  40525  lhe4.4ex1a  40681  stoweidlem26  42331  stoweidlem34  42339  smfmullem2  43087  fmtno5lem4  43738  fmtno5  43739  fmtno5faclem2  43762  3ndvds4  43778  139prmALT  43779  31prm  43780  m5prm  43781  11t31e341  43917  2exp340mod341  43918  8exp8mod9  43921  sbgoldbalt  43966  sbgoldbo  43972  nnsum3primesle9  43979  nnsum4primeseven  43985  nnsum4primesevenALTV  43986