Theorem 4p1e5 11784

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

Syntax hints:   = wceq 1537  (class class class)co 7156  1c1 10538   + caddc 10540  4c4 11695  5c5 11696

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814  df-5 11704

This theorem is referenced by:  8t7e56  12219  9t6e54  12225  s5len  14262  bpoly4  15413  2exp16  16424  prmlem2  16453  163prm  16458  317prm  16459  631prm  16460  1259lem1  16464  1259lem2  16465  1259lem3  16466  1259lem4  16467  2503lem1  16470  2503lem2  16471  2503lem3  16472  4001lem1  16474  4001lem2  16475  4001lem3  16476  4001lem4  16477  log2ublem3  25526  log2ub  25527  ex-exp  28229  ex-fac  28230  fib5  31663  fib6  31664  hgt750lemd  31919  hgt750lem2  31923  3cubeslem3l  39303  3cubeslem3r  39304  fmtno1  43723  257prm  43743  fmtno4prmfac  43754  fmtno4nprmfac193  43756  fmtno5faclem2  43762  31prm  43780  127prm  43783  m11nprm  43786  2exp340mod341  43918  nnsum3primesle9  43979  5m4e1  44918