Theorem 4p1e5 11825

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

Syntax hints:   = wceq 1538  (class class class)co 7155  1c1 10581   + caddc 10583  4c4 11736  5c5 11737

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2750  df-5 11745

This theorem is referenced by:  8t7e56  12262  9t6e54  12268  s5len  14314  bpoly4  15466  2exp16  16487  prmlem2  16516  163prm  16521  317prm  16522  631prm  16523  1259lem1  16527  1259lem2  16528  1259lem3  16529  1259lem4  16530  2503lem1  16533  2503lem2  16534  2503lem3  16535  4001lem1  16537  4001lem2  16538  4001lem3  16539  4001lem4  16540  log2ublem3  25638  log2ub  25639  ex-exp  28339  ex-fac  28340  fib5  31895  fib6  31896  hgt750lemd  32151  hgt750lem2  32155  60gcd7e1  39598  3lexlogpow5ineq1  39647  3lexlogpow5ineq5  39653  aks4d1p1p4  39663  aks4d1p1p7  39666  aks4d1p1  39668  5bc2eq10  39669  2ap1caineq  39672  3cubeslem3l  40028  3cubeslem3r  40029  fmtno1  44454  257prm  44474  fmtno4prmfac  44485  fmtno4nprmfac193  44487  fmtno5faclem2  44493  31prm  44510  127prm  44512  m11nprm  44514  2exp340mod341  44646  nnsum3primesle9  44707  5m4e1  45789