Theorem 5p1e6 12513

Description: 5 + 1 = 6. (Contributed by Mario Carneiro, 18-Apr-2015.)

Assertion

Ref	Expression
5p1e6	⊢ (5 + 1) = 6

Proof of Theorem 5p1e6

Step	Hyp	Ref	Expression
1		df-6 12433	. 2 ⊢ 6 = (5 + 1)
2	1	eqcomi 2772	1 ⊢ (5 + 1) = 6

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7440  1c1 11225   + caddc 11227  5c5 12424  6c6 12425

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-6 12433

This theorem is used by:  8t8e64  12964  9t7e63  12970  5recm6rec  12988  fldiv4p1lem1div2  13999  s6len  15078  5ndvds6  16610  163prm  17329  631prm  17331  1259lem1  17335  1259lem4  17338  2503lem1  17341  2503lem2  17342  4001lem1  17345  4001lem4  17348  4001prm  17349  log2ublem3  27303  log2ub  27304  fib6  35105  hgt750lemd  35344  hgt750lem2  35348  60gcd7e1  43246  12lcm5e60  43249  3lexlogpow5ineq1  43295  3lexlogpow5ineq5  43301  aks4d1p1  43317  1p5e6  43503  3cubeslem3l  43887  fmtno5lem2  48842  fmtno5lem3  48843  fmtno5lem4  48844  fmtno4prmfac193  48861  fmtno4nprmfac193  48862  fmtno5faclem3  48869  flsqrt5  48882  127prm  48887  ppivalnnnprm  48916  gbowge7  49064  gbege6  49066  sbgoldbwt  49078  nnsum3primesle9  49095  veronesevrowd  51257  veroquadgsumlem  51261