Theorem 5p1e6 12444

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 12364	. 2 ⊢ 6 = (5 + 1)
2	1	eqcomi 2769	1 ⊢ (5 + 1) = 6

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7409  1c1 11158   + caddc 11160  5c5 12355  6c6 12356

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 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-6 12364

This theorem is used by:  8t8e64  12895  9t7e63  12901  5recm6rec  12919  fldiv4p1lem1div2  13929  s6len  15005  5ndvds6  16537  163prm  17250  631prm  17252  1259lem1  17256  1259lem4  17259  2503lem1  17262  2503lem2  17263  4001lem1  17266  4001lem4  17269  4001prm  17270  log2ublem3  27225  log2ub  27226  fib6  34958  hgt750lemd  35197  hgt750lem2  35201  60gcd7e1  42969  12lcm5e60  42972  3lexlogpow5ineq1  43018  3lexlogpow5ineq5  43024  aks4d1p1  43040  1p5e6  43226  3cubeslem3l  43629  fmtno5lem2  48555  fmtno5lem3  48556  fmtno5lem4  48557  fmtno4prmfac193  48574  fmtno4nprmfac193  48575  fmtno5faclem3  48582  flsqrt5  48595  127prm  48600  ppivalnnnprm  48629  gbowge7  48777  gbege6  48779  sbgoldbwt  48791  nnsum3primesle9  48808  veronesevrowd  50895  veroquadgsumlem  50899