Theorem 4p1e5 12322

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

Syntax hints:   = wceq 1542  (class class class)co 7367  1c1 11039   + caddc 11041  4c4 12238  5c5 12239

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

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

This theorem is referenced by:  8t7e56  12764  9t6e54  12770  s5len  14862  bpoly4  16024  2exp16  17061  prmlem2  17090  163prm  17095  317prm  17096  631prm  17097  1259lem1  17101  1259lem2  17102  1259lem3  17103  1259lem4  17104  2503lem1  17107  2503lem2  17108  2503lem3  17109  4001lem1  17111  4001lem2  17112  4001lem3  17113  4001lem4  17114  log2ublem3  26912  log2ub  26913  ex-exp  30520  ex-fac  30521  fib5  34549  fib6  34550  hgt750lemd  34792  hgt750lem2  34796  60gcd7e1  42444  3lexlogpow5ineq1  42493  3lexlogpow5ineq5  42499  aks4d1p1p4  42510  aks4d1p1p7  42513  aks4d1p1  42515  5bc2eq10  42581  2ap1caineq  42584  sq45  43104  3cubeslem3l  43118  3cubeslem3r  43119  sin5tlem4  47324  goldratmolem2  47334  fmtno1  48004  257prm  48024  fmtno4prmfac  48035  fmtno4nprmfac193  48037  fmtno5faclem2  48043  31prm  48060  127prm  48062  m11nprm  48064  ppivalnnnprm  48091  2exp340mod341  48209  nnsum3primesle9  48270  5m4e1  50272