Theorem 4p1e5 12024

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

Syntax hints:   = wceq 1543  (class class class)co 7252  1c1 10778   + caddc 10780  4c4 11935  5c5 11936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-9 2122  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2731  df-5 11944

This theorem is referenced by:  8t7e56  12461  9t6e54  12467  s5len  14516  bpoly4  15672  2exp16  16695  prmlem2  16724  163prm  16729  317prm  16730  631prm  16731  1259lem1  16735  1259lem2  16736  1259lem3  16737  1259lem4  16738  2503lem1  16741  2503lem2  16742  2503lem3  16743  4001lem1  16745  4001lem2  16746  4001lem3  16747  4001lem4  16748  log2ublem3  25978  log2ub  25979  ex-exp  28690  ex-fac  28691  fib5  32247  fib6  32248  hgt750lemd  32503  hgt750lem2  32507  60gcd7e1  39920  3lexlogpow5ineq1  39969  3lexlogpow5ineq5  39975  aks4d1p1p4  39985  aks4d1p1p7  39988  aks4d1p1  39990  5bc2eq10  39998  2ap1caineq  40001  3cubeslem3l  40396  3cubeslem3r  40397  fmtno1  44854  257prm  44874  fmtno4prmfac  44885  fmtno4nprmfac193  44887  fmtno5faclem2  44893  31prm  44910  127prm  44912  m11nprm  44914  2exp340mod341  45046  nnsum3primesle9  45107  5m4e1  46360