Theorem 4p1e5 12410

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

Syntax hints:   = wceq 1537  (class class class)co 7431  1c1 11154   + caddc 11156  4c4 12321  5c5 12322

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727  df-5 12330

This theorem is referenced by:  8t7e56  12851  9t6e54  12857  s5len  14936  bpoly4  16092  2exp16  17125  prmlem2  17154  163prm  17159  317prm  17160  631prm  17161  1259lem1  17165  1259lem2  17166  1259lem3  17167  1259lem4  17168  2503lem1  17171  2503lem2  17172  2503lem3  17173  4001lem1  17175  4001lem2  17176  4001lem3  17177  4001lem4  17178  log2ublem3  27006  log2ub  27007  ex-exp  30479  ex-fac  30480  fib5  34387  fib6  34388  hgt750lemd  34642  hgt750lem2  34646  60gcd7e1  41987  3lexlogpow5ineq1  42036  3lexlogpow5ineq5  42042  aks4d1p1p4  42053  aks4d1p1p7  42056  aks4d1p1  42058  5bc2eq10  42124  2ap1caineq  42127  sq45  42658  3cubeslem3l  42674  3cubeslem3r  42675  fmtno1  47466  257prm  47486  fmtno4prmfac  47497  fmtno4nprmfac193  47499  fmtno5faclem2  47505  31prm  47522  127prm  47524  m11nprm  47526  2exp340mod341  47658  nnsum3primesle9  47719  5m4e1  49028