Theorem 4p1e5 12286

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

Syntax hints:   = wceq 1541  (class class class)co 7358  1c1 11027   + caddc 11029  4c4 12202  5c5 12203

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 2708

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

This theorem is referenced by:  8t7e56  12727  9t6e54  12733  s5len  14823  bpoly4  15982  2exp16  17018  prmlem2  17047  163prm  17052  317prm  17053  631prm  17054  1259lem1  17058  1259lem2  17059  1259lem3  17060  1259lem4  17061  2503lem1  17064  2503lem2  17065  2503lem3  17066  4001lem1  17068  4001lem2  17069  4001lem3  17070  4001lem4  17071  log2ublem3  26914  log2ub  26915  ex-exp  30525  ex-fac  30526  fib5  34562  fib6  34563  hgt750lemd  34805  hgt750lem2  34809  60gcd7e1  42259  3lexlogpow5ineq1  42308  3lexlogpow5ineq5  42314  aks4d1p1p4  42325  aks4d1p1p7  42328  aks4d1p1  42330  5bc2eq10  42396  2ap1caineq  42399  sq45  42914  3cubeslem3l  42928  3cubeslem3r  42929  fmtno1  47787  257prm  47807  fmtno4prmfac  47818  fmtno4nprmfac193  47820  fmtno5faclem2  47826  31prm  47843  127prm  47845  m11nprm  47847  2exp340mod341  47979  nnsum3primesle9  48040  5m4e1  50042