Theorem 4p1e5 12489

Description: 4 + 1 = 5. (Contributed by Mario Carneiro, 18-Apr-2015.)

Assertion

Ref	Expression
4p1e5	⊢ (4 + 1) = 5

Proof of Theorem 4p1e5

Step	Hyp	Ref	Expression
1		df-5 12409	. 2 ⊢ 5 = (4 + 1)
2	1	eqcomi 2770	1 ⊢ (4 + 1) = 5

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7421  1c1 11202   + caddc 11204  4c4 12400  5c5 12401

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-5 12409

This theorem is used by:  8t7e56  12940  9t6e54  12946  s5len  15052  bpoly4  16226  2exp16  17269  prmlem2  17299  163prm  17304  317prm  17305  631prm  17306  1259lem1  17310  1259lem2  17311  1259lem3  17312  1259lem4  17313  2503lem1  17316  2503lem2  17317  2503lem3  17318  4001lem1  17320  4001lem2  17321  4001lem3  17322  4001lem4  17323  log2ublem3  27277  log2ub  27278  ex-exp  31052  ex-fac  31053  fib5  35038  fib6  35039  hgt750lemd  35278  hgt750lem2  35282  60gcd7e1  43057  3lexlogpow5ineq1  43106  3lexlogpow5ineq5  43112  aks4d1p1p4  43123  aks4d1p1p7  43126  aks4d1p1  43128  5bc2eq10  43194  2ap1caineq  43197  25or6to4  43258  1p4e5  43313  sq45  43684  3cubeslem3l  43698  3cubeslem3r  43699  sin5tlem4  47923  goldratmolem2  47934  fmtno1  48627  257prm  48647  fmtno4prmfac  48658  fmtno4nprmfac193  48660  fmtno5faclem2  48666  31prm  48683  127prm  48685  m11nprm  48687  ppivalnnnprm  48714  2exp340mod341  48832  nnsum3primesle9  48893  5m4e1  50936  veronesevrowd  50980  veroquadgsumlem  50984