Theorem 4p1e5 12316

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

Syntax hints:   = wceq 1542  (class class class)co 7361  1c1 11033   + caddc 11035  4c4 12232  5c5 12233

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 2709

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

This theorem is referenced by:  8t7e56  12758  9t6e54  12764  s5len  14856  bpoly4  16018  2exp16  17055  prmlem2  17084  163prm  17089  317prm  17090  631prm  17091  1259lem1  17095  1259lem2  17096  1259lem3  17097  1259lem4  17098  2503lem1  17101  2503lem2  17102  2503lem3  17103  4001lem1  17105  4001lem2  17106  4001lem3  17107  4001lem4  17108  log2ublem3  26928  log2ub  26929  ex-exp  30538  ex-fac  30539  fib5  34568  fib6  34569  hgt750lemd  34811  hgt750lem2  34815  60gcd7e1  42461  3lexlogpow5ineq1  42510  3lexlogpow5ineq5  42516  aks4d1p1p4  42527  aks4d1p1p7  42530  aks4d1p1  42532  5bc2eq10  42598  2ap1caineq  42601  sq45  43121  3cubeslem3l  43135  3cubeslem3r  43136  sin5tlem4  47343  fmtno1  48019  257prm  48039  fmtno4prmfac  48050  fmtno4nprmfac193  48052  fmtno5faclem2  48058  31prm  48075  127prm  48077  m11nprm  48079  ppivalnnnprm  48106  2exp340mod341  48224  nnsum3primesle9  48285  5m4e1  50287