Theorem 4p1e5 11771

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

Syntax hints:   = wceq 1538  (class class class)co 7135  1c1 10527   + caddc 10529  4c4 11682  5c5 11683

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 2770

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

This theorem is referenced by:  8t7e56  12206  9t6e54  12212  s5len  14253  bpoly4  15405  2exp16  16416  prmlem2  16445  163prm  16450  317prm  16451  631prm  16452  1259lem1  16456  1259lem2  16457  1259lem3  16458  1259lem4  16459  2503lem1  16462  2503lem2  16463  2503lem3  16464  4001lem1  16466  4001lem2  16467  4001lem3  16468  4001lem4  16469  log2ublem3  25534  log2ub  25535  ex-exp  28235  ex-fac  28236  fib5  31773  fib6  31774  hgt750lemd  32029  hgt750lem2  32033  60gcd7e1  39293  3lexlogpow5ineq1  39341  5bc2eq10  39346  2ap1caineq  39349  3cubeslem3l  39627  3cubeslem3r  39628  fmtno1  44058  257prm  44078  fmtno4prmfac  44089  fmtno4nprmfac193  44091  fmtno5faclem2  44097  31prm  44114  127prm  44116  m11nprm  44119  2exp340mod341  44251  nnsum3primesle9  44312  5m4e1  45325