Theorem 4p1e5 12284

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

Syntax hints:   = wceq 1541  (class class class)co 7356  1c1 11025   + caddc 11027  4c4 12200  5c5 12201

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2726  df-5 12209

This theorem is referenced by:  8t7e56  12725  9t6e54  12731  s5len  14821  bpoly4  15980  2exp16  17016  prmlem2  17045  163prm  17050  317prm  17051  631prm  17052  1259lem1  17056  1259lem2  17057  1259lem3  17058  1259lem4  17059  2503lem1  17062  2503lem2  17063  2503lem3  17064  4001lem1  17066  4001lem2  17067  4001lem3  17068  4001lem4  17069  log2ublem3  26912  log2ub  26913  ex-exp  30474  ex-fac  30475  fib5  34511  fib6  34512  hgt750lemd  34754  hgt750lem2  34758  60gcd7e1  42198  3lexlogpow5ineq1  42247  3lexlogpow5ineq5  42253  aks4d1p1p4  42264  aks4d1p1p7  42267  aks4d1p1  42269  5bc2eq10  42335  2ap1caineq  42338  sq45  42856  3cubeslem3l  42870  3cubeslem3r  42871  fmtno1  47729  257prm  47749  fmtno4prmfac  47760  fmtno4nprmfac193  47762  fmtno5faclem2  47768  31prm  47785  127prm  47787  m11nprm  47789  2exp340mod341  47921  nnsum3primesle9  47982  5m4e1  49984