Theorem 4p1e5 12298

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

Syntax hints:   = wceq 1542  (class class class)co 7368  1c1 11039   + caddc 11041  4c4 12214  5c5 12215

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 12223

This theorem is referenced by:  8t7e56  12739  9t6e54  12745  s5len  14835  bpoly4  15994  2exp16  17030  prmlem2  17059  163prm  17064  317prm  17065  631prm  17066  1259lem1  17070  1259lem2  17071  1259lem3  17072  1259lem4  17073  2503lem1  17076  2503lem2  17077  2503lem3  17078  4001lem1  17080  4001lem2  17081  4001lem3  17082  4001lem4  17083  log2ublem3  26926  log2ub  26927  ex-exp  30537  ex-fac  30538  fib5  34583  fib6  34584  hgt750lemd  34826  hgt750lem2  34830  60gcd7e1  42375  3lexlogpow5ineq1  42424  3lexlogpow5ineq5  42430  aks4d1p1p4  42441  aks4d1p1p7  42444  aks4d1p1  42446  5bc2eq10  42512  2ap1caineq  42515  sq45  43029  3cubeslem3l  43043  3cubeslem3r  43044  fmtno1  47901  257prm  47921  fmtno4prmfac  47932  fmtno4nprmfac193  47934  fmtno5faclem2  47940  31prm  47957  127prm  47959  m11nprm  47961  2exp340mod341  48093  nnsum3primesle9  48154  5m4e1  50156