Theorem 3p1e4 12409

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

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7413  1c1 11125   + caddc 11127  3c3 12320  4c4 12321

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-4 12329

This theorem is used by:  7t6e42  12854  8t5e40  12859  9t5e45  12866  fz0to4untppr  13685  fz0to5un2tp  13686  fac4  14345  hash4  14471  hash7g  14551  s4len  14970  bpoly4  16145  2exp16  17182  43prm  17214  83prm  17215  317prm  17218  1259lem2  17224  1259lem3  17225  1259lem4  17226  1259lem5  17227  2503lem1  17229  2503lem2  17230  4001lem1  17233  4001lem2  17234  4001lem4  17236  4001prm  17237  binom4  27087  quartlem1  27094  log2ublem3  27185  log2ub  27186  bclbnd  27516  addsqnreup  27679  tgcgr4  28873  upgr4cycl4dv4e  30665  ex-opab  30912  ex-ind-dvds  30941  evl1deg3  33988  iconstr  34276  cos9thpiminplylem1  34292  fib4  34915  fib5  34916  hgt750lem  35159  hgt750lem2  35160  3lexlogpow5ineq1  42920  3lexlogpow5ineq5  42926  aks4d1p1p5  42941  aks4d1p1  42942  1p3e4  43126  235t711  43180  3cubeslem3l  43531  3cubeslem3r  43532  inductionexd  44995  lhe4.4ex1a  45153  stoweidlem26  46854  stoweidlem34  46862  smfmullem2  47620  2ltceilhalf  48220  fmtno5lem4  48459  fmtno5  48460  fmtno5faclem2  48483  3ndvds4  48498  139prmALT  48499  31prm  48500  m5prm  48501  ppivalnnnprm  48531  11t31e341  48648  2exp340mod341  48649  8exp8mod9  48652  sbgoldbalt  48697  sbgoldbo  48703  nnsum3primesle9  48710  nnsum4primeseven  48716  nnsum4primesevenALTV  48717  gpgprismgr4cycllem10  49020  ackval3  49613  ackval3012  49622  ackval41a  49624  ackval41  49625  ackval42  49626  veronesevrowd  50812  veroquadgsumlem  50816