Theorem 4p1e5 12311

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

Syntax hints:   = wceq 1542  (class class class)co 7358  1c1 11028   + caddc 11030  4c4 12227  5c5 12228

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 12236

This theorem is referenced by:  8t7e56  12753  9t6e54  12759  s5len  14851  bpoly4  16013  2exp16  17050  prmlem2  17079  163prm  17084  317prm  17085  631prm  17086  1259lem1  17090  1259lem2  17091  1259lem3  17092  1259lem4  17093  2503lem1  17096  2503lem2  17097  2503lem3  17098  4001lem1  17100  4001lem2  17101  4001lem3  17102  4001lem4  17103  log2ublem3  26929  log2ub  26930  ex-exp  30540  ex-fac  30541  fib5  34570  fib6  34571  hgt750lemd  34813  hgt750lem2  34817  60gcd7e1  42455  3lexlogpow5ineq1  42504  3lexlogpow5ineq5  42510  aks4d1p1p4  42521  aks4d1p1p7  42524  aks4d1p1  42526  5bc2eq10  42592  2ap1caineq  42595  sq45  43115  3cubeslem3l  43129  3cubeslem3r  43130  fmtno1  48001  257prm  48021  fmtno4prmfac  48032  fmtno4nprmfac193  48034  fmtno5faclem2  48040  31prm  48057  127prm  48059  m11nprm  48061  ppivalnnnprm  48088  2exp340mod341  48206  nnsum3primesle9  48267  5m4e1  50269