Theorem 4p1e5 12528

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

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7451  1c1 11240   + caddc 11242  4c4 12439  5c5 12440

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-5 12448

This theorem is used by:  8t7e56  12979  9t6e54  12985  s5len  15094  bpoly4  16269  2exp16  17312  prmlem2  17342  163prm  17347  317prm  17348  631prm  17349  1259lem1  17353  1259lem2  17354  1259lem3  17355  1259lem4  17356  2503lem1  17359  2503lem2  17360  2503lem3  17361  4001lem1  17363  4001lem2  17364  4001lem3  17365  4001lem4  17366  log2ublem3  27333  log2ub  27334  ex-exp  31108  ex-fac  31109  fib5  35148  fib6  35149  hgt750lemd  35388  hgt750lem2  35392  60gcd7e1  43321  3lexlogpow5ineq1  43370  3lexlogpow5ineq5  43376  aks4d1p1p4  43387  aks4d1p1p7  43390  aks4d1p1  43392  5bc2eq10  43458  2ap1caineq  43461  25or6to4  43522  1p4e5  43577  sq45  43948  3cubeslem3l  43962  3cubeslem3r  43963  sin5tlem4  48195  goldratmolem2  48206  fmtno1  48899  257prm  48919  fmtno4prmfac  48930  fmtno4nprmfac193  48932  fmtno5faclem2  48938  31prm  48955  127prm  48957  m11nprm  48959  ppivalnnnprm  48986  2exp340mod341  49104  nnsum3primesle9  49165  5m4e1  51363  veronesevrowd  51407  veroquadgsumlem  51411