Theorem 4p1e5 12498

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

This proof depends on syntax axioms:   = wceq 1569  (class class class)co 7427  1c1 11211   + caddc 11213  4c4 12409  5c5 12410

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 1944  ax-6 2001  ax-7 2042  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2755  df-5 12418

This theorem is used by:  8t7e56  12949  9t6e54  12955  s5len  15063  bpoly4  16237  2exp16  17280  prmlem2  17310  163prm  17315  317prm  17316  631prm  17317  1259lem1  17321  1259lem2  17322  1259lem3  17323  1259lem4  17324  2503lem1  17327  2503lem2  17328  2503lem3  17329  4001lem1  17331  4001lem2  17332  4001lem3  17333  4001lem4  17334  log2ublem3  27288  log2ub  27289  ex-exp  31063  ex-fac  31064  fib5  35090  fib6  35091  hgt750lemd  35330  hgt750lem2  35334  60gcd7e1  43195  3lexlogpow5ineq1  43244  3lexlogpow5ineq5  43250  aks4d1p1p4  43261  aks4d1p1p7  43264  aks4d1p1  43266  5bc2eq10  43332  2ap1caineq  43335  25or6to4  43396  1p4e5  43451  sq45  43822  3cubeslem3l  43836  3cubeslem3r  43837  sin5tlem4  48061  goldratmolem2  48072  fmtno1  48765  257prm  48785  fmtno4prmfac  48796  fmtno4nprmfac193  48798  fmtno5faclem2  48804  31prm  48821  127prm  48823  m11nprm  48825  ppivalnnnprm  48852  2exp340mod341  48970  nnsum3primesle9  49031  5m4e1  51149  veronesevrowd  51193  veroquadgsumlem  51197