Theorem 3p1e4 12411

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

Syntax hints:   = wceq 1540  (class class class)co 7431  1c1 11156   + caddc 11158  3c3 12322  4c4 12323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-4 12331

This theorem is referenced by:  7t6e42  12846  8t5e40  12851  9t5e45  12858  fz0to4untppr  13670  fz0to5un2tp  13671  fac4  14320  hash4  14446  hash7g  14525  s4len  14938  bpoly4  16095  2exp16  17128  43prm  17159  83prm  17160  317prm  17163  1259lem2  17169  1259lem3  17170  1259lem4  17171  1259lem5  17172  2503lem1  17174  2503lem2  17175  4001lem1  17178  4001lem2  17179  4001lem4  17181  4001prm  17182  binom4  26893  quartlem1  26900  log2ublem3  26991  log2ub  26992  bclbnd  27324  addsqnreup  27487  tgcgr4  28539  upgr4cycl4dv4e  30204  ex-opab  30451  ex-ind-dvds  30480  evl1deg3  33603  fib4  34406  fib5  34407  hgt750lem  34666  hgt750lem2  34667  3lexlogpow5ineq1  42055  3lexlogpow5ineq5  42061  aks4d1p1p5  42076  aks4d1p1  42077  235t711  42339  3cubeslem3l  42697  3cubeslem3r  42698  inductionexd  44168  lhe4.4ex1a  44348  stoweidlem26  46041  stoweidlem34  46049  smfmullem2  46807  fmtno5lem4  47543  fmtno5  47544  fmtno5faclem2  47567  3ndvds4  47582  139prmALT  47583  31prm  47584  m5prm  47585  11t31e341  47719  2exp340mod341  47720  8exp8mod9  47723  sbgoldbalt  47768  sbgoldbo  47774  nnsum3primesle9  47781  nnsum4primeseven  47787  nnsum4primesevenALTV  47788  2ltceilhalf  48015  ackval3  48604  ackval3012  48613  ackval41a  48615  ackval41  48616  ackval42  48617