Theorem 3p1e4 12494

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

This proof depends on syntax axioms:   = wceq 1569  (class class class)co 7424  1c1 11208   + caddc 11210  3c3 12405  4c4 12406

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

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

This theorem is used by:  7t6e42  12939  8t5e40  12944  9t5e45  12951  fz0to4untppr  13771  fz0to5un2tp  13772  fac4  14432  hash4  14558  hash7g  14638  s4len  15059  bpoly4  16234  2exp16  17277  43prm  17309  83prm  17310  317prm  17313  1259lem2  17319  1259lem3  17320  1259lem4  17321  1259lem5  17322  2503lem1  17324  2503lem2  17325  4001lem1  17328  4001lem2  17329  4001lem4  17331  4001prm  17332  binom4  27187  quartlem1  27194  log2ublem3  27285  log2ub  27286  bclbnd  27616  addsqnreup  27779  tgcgr4  29003  upgr4cycl4dv4e  30795  ex-opab  31042  ex-ind-dvds  31071  evl1deg3  34160  iconstr  34448  cos9thpiminplylem1  34464  fib4  35086  fib5  35087  hgt750lem  35330  hgt750lem2  35331  3lexlogpow5ineq1  43213  3lexlogpow5ineq5  43219  aks4d1p1p5  43234  aks4d1p1  43235  1p3e4  43419  235t711  43471  3cubeslem3l  43805  3cubeslem3r  43806  inductionexd  45264  lhe4.4ex1a  45422  stoweidlem26  47144  stoweidlem34  47152  smfmullem2  47910  2ltceilhalf  48510  fmtno5lem4  48749  fmtno5  48750  fmtno5faclem2  48773  3ndvds4  48788  139prmALT  48789  31prm  48790  m5prm  48791  ppivalnnnprm  48821  11t31e341  48938  2exp340mod341  48939  8exp8mod9  48942  sbgoldbalt  48987  sbgoldbo  48993  nnsum3primesle9  49000  nnsum4primeseven  49006  nnsum4primesevenALTV  49007  gpgprismgr4cycllem10  49310  ackval3  49903  ackval3012  49912  ackval41a  49914  ackval41  49915  ackval42  49916  veronesevrowd  51162  veroquadgsumlem  51166