Theorem 4p1e5 12356

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

Syntax hints:   = wceq 1533  (class class class)co 7402  1c1 11108   + caddc 11110  4c4 12267  5c5 12268

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1774  df-cleq 2716  df-5 12276

This theorem is referenced by:  8t7e56  12795  9t6e54  12801  s5len  14849  bpoly4  16001  2exp16  17025  prmlem2  17054  163prm  17059  317prm  17060  631prm  17061  1259lem1  17065  1259lem2  17066  1259lem3  17067  1259lem4  17068  2503lem1  17071  2503lem2  17072  2503lem3  17073  4001lem1  17075  4001lem2  17076  4001lem3  17077  4001lem4  17078  log2ublem3  26799  log2ub  26800  ex-exp  30175  ex-fac  30176  fib5  33896  fib6  33897  hgt750lemd  34151  hgt750lem2  34155  60gcd7e1  41367  3lexlogpow5ineq1  41416  3lexlogpow5ineq5  41422  aks4d1p1p4  41433  aks4d1p1p7  41436  aks4d1p1  41438  5bc2eq10  41455  2ap1caineq  41458  sq45  41927  3cubeslem3l  41938  3cubeslem3r  41939  fmtno1  46719  257prm  46739  fmtno4prmfac  46750  fmtno4nprmfac193  46752  fmtno5faclem2  46758  31prm  46775  127prm  46777  m11nprm  46779  2exp340mod341  46911  nnsum3primesle9  46972  5m4e1  48056