Theorem 4p1e5 12413

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

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7414  1c1 11128   + caddc 11130  4c4 12324  5c5 12325

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-5 12333

This theorem is used by:  8t7e56  12864  9t6e54  12870  s5len  14974  bpoly4  16148  2exp16  17185  prmlem2  17215  163prm  17220  317prm  17221  631prm  17222  1259lem1  17226  1259lem2  17227  1259lem3  17228  1259lem4  17229  2503lem1  17232  2503lem2  17233  2503lem3  17234  4001lem1  17236  4001lem2  17237  4001lem3  17238  4001lem4  17239  log2ublem3  27188  log2ub  27189  ex-exp  30933  ex-fac  30934  fib5  34919  fib6  34920  hgt750lemd  35159  hgt750lem2  35163  60gcd7e1  42874  3lexlogpow5ineq1  42923  3lexlogpow5ineq5  42929  aks4d1p1p4  42940  aks4d1p1p7  42943  aks4d1p1  42945  5bc2eq10  43011  2ap1caineq  43014  25or6to4  43075  1p4e5  43130  sq45  43520  3cubeslem3l  43534  3cubeslem3r  43535  sin5tlem4  47743  goldratmolem2  47754  fmtno1  48447  257prm  48467  fmtno4prmfac  48478  fmtno4nprmfac193  48480  fmtno5faclem2  48486  31prm  48503  127prm  48505  m11nprm  48507  ppivalnnnprm  48534  2exp340mod341  48652  nnsum3primesle9  48713  5m4e1  50771  veronesevrowd  50815  veroquadgsumlem  50819