Theorem 4p1e5 12308

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

Syntax hints:   = wceq 1541  (class class class)co 7362  1c1 11061   + caddc 11063  4c4 12219  5c5 12220

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723  df-5 12228

This theorem is referenced by:  8t7e56  12747  9t6e54  12753  s5len  14801  bpoly4  15953  2exp16  16974  prmlem2  17003  163prm  17008  317prm  17009  631prm  17010  1259lem1  17014  1259lem2  17015  1259lem3  17016  1259lem4  17017  2503lem1  17020  2503lem2  17021  2503lem3  17022  4001lem1  17024  4001lem2  17025  4001lem3  17026  4001lem4  17027  log2ublem3  26335  log2ub  26336  ex-exp  29457  ex-fac  29458  fib5  33094  fib6  33095  hgt750lemd  33350  hgt750lem2  33354  60gcd7e1  40535  3lexlogpow5ineq1  40584  3lexlogpow5ineq5  40590  aks4d1p1p4  40601  aks4d1p1p7  40604  aks4d1p1  40606  5bc2eq10  40623  2ap1caineq  40626  3cubeslem3l  41067  3cubeslem3r  41068  fmtno1  45853  257prm  45873  fmtno4prmfac  45884  fmtno4nprmfac193  45886  fmtno5faclem2  45892  31prm  45909  127prm  45911  m11nprm  45913  2exp340mod341  46045  nnsum3primesle9  46106  5m4e1  47364