Theorem 3p1e4 12023

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

Syntax hints:   = wceq 1543  (class class class)co 7252  1c1 10778   + caddc 10780  3c3 11934  4c4 11935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-9 2122  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2731  df-4 11943

This theorem is referenced by:  7t6e42  12454  8t5e40  12459  9t5e45  12466  fac4  13898  hash4  14025  s4len  14515  bpoly4  15672  2exp16  16695  43prm  16726  83prm  16727  317prm  16730  1259lem2  16736  1259lem3  16737  1259lem4  16738  1259lem5  16739  2503lem1  16741  2503lem2  16742  4001lem1  16745  4001lem2  16746  4001lem4  16748  4001prm  16749  binom4  25880  quartlem1  25887  log2ublem3  25978  log2ub  25979  bclbnd  26308  addsqnreup  26471  tgcgr4  26771  upgr4cycl4dv4e  28425  ex-opab  28672  ex-ind-dvds  28701  fib4  32246  fib5  32247  hgt750lem  32506  hgt750lem2  32507  3lexlogpow5ineq1  39969  3lexlogpow5ineq5  39975  aks4d1p1p5  39989  aks4d1p1  39990  235t711  40212  3cubeslem3l  40396  3cubeslem3r  40397  inductionexd  41627  lhe4.4ex1a  41809  stoweidlem26  43430  stoweidlem34  43438  smfmullem2  44186  fmtno5lem4  44869  fmtno5  44870  fmtno5faclem2  44893  3ndvds4  44908  139prmALT  44909  31prm  44910  m5prm  44911  11t31e341  45045  2exp340mod341  45046  8exp8mod9  45049  sbgoldbalt  45094  sbgoldbo  45100  nnsum3primesle9  45107  nnsum4primeseven  45113  nnsum4primesevenALTV  45114  ackval3  45890  ackval3012  45899  ackval41a  45901  ackval41  45902  ackval42  45903