Theorem 3p1e4 12527

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

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7451  1c1 11240   + caddc 11242  3c3 12438  4c4 12439

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  7t6e42  12972  8t5e40  12977  9t5e45  12984  fz0to4untppr  13804  fz0to5un2tp  13805  fac4  14466  hash4  14592  hash7g  14672  s4len  15093  bpoly4  16269  2exp16  17312  43prm  17344  83prm  17345  317prm  17348  1259lem2  17354  1259lem3  17355  1259lem4  17356  1259lem5  17357  2503lem1  17359  2503lem2  17360  4001lem1  17363  4001lem2  17364  4001lem4  17366  4001prm  17367  binom4  27235  quartlem1  27242  log2ublem3  27333  log2ub  27334  bclbnd  27664  addsqnreup  27827  tgcgr4  29051  upgr4cycl4dv4e  30843  ex-opab  31090  ex-ind-dvds  31119  evl1deg3  34213  iconstr  34509  cos9thpiminplylem1  34525  fib4  35147  fib5  35148  hgt750lem  35391  hgt750lem2  35392  3lexlogpow5ineq1  43370  3lexlogpow5ineq5  43376  aks4d1p1p5  43391  aks4d1p1  43392  1p3e4  43576  235t711  43628  3cubeslem3l  43962  3cubeslem3r  43963  inductionexd  45416  lhe4.4ex1a  45574  stoweidlem26  47309  stoweidlem34  47317  smfmullem2  48075  2ltceilhalf  48675  fmtno5lem4  48914  fmtno5  48915  fmtno5faclem2  48938  3ndvds4  48953  139prmALT  48954  31prm  48955  m5prm  48956  ppivalnnnprm  48986  11t31e341  49103  2exp340mod341  49104  8exp8mod9  49107  sbgoldbalt  49152  sbgoldbo  49158  nnsum3primesle9  49165  nnsum4primeseven  49171  nnsum4primesevenALTV  49172  gpgprismgr4cycllem10  49475  ackval3  50126  ackval3012  50135  ackval41a  50137  ackval41  50138  ackval42  50139  veronesevrowd  51407  veroquadgsumlem  51411