Theorem 4p1e5 12413

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

Syntax hints:   = wceq 1539  (class class class)co 7432  1c1 11157   + caddc 11159  4c4 12324  5c5 12325

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2728  df-5 12333

This theorem is referenced by:  8t7e56  12855  9t6e54  12861  s5len  14940  bpoly4  16096  2exp16  17129  prmlem2  17158  163prm  17163  317prm  17164  631prm  17165  1259lem1  17169  1259lem2  17170  1259lem3  17171  1259lem4  17172  2503lem1  17175  2503lem2  17176  2503lem3  17177  4001lem1  17179  4001lem2  17180  4001lem3  17181  4001lem4  17182  log2ublem3  26992  log2ub  26993  ex-exp  30470  ex-fac  30471  fib5  34408  fib6  34409  hgt750lemd  34664  hgt750lem2  34668  60gcd7e1  42007  3lexlogpow5ineq1  42056  3lexlogpow5ineq5  42062  aks4d1p1p4  42073  aks4d1p1p7  42076  aks4d1p1  42078  5bc2eq10  42144  2ap1caineq  42147  sq45  42686  3cubeslem3l  42702  3cubeslem3r  42703  fmtno1  47533  257prm  47553  fmtno4prmfac  47564  fmtno4nprmfac193  47566  fmtno5faclem2  47572  31prm  47589  127prm  47591  m11nprm  47593  2exp340mod341  47725  nnsum3primesle9  47786  5m4e1  49371