Theorem 5p1e6 12489

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

This proof depends on syntax axioms:   = wceq 1569  (class class class)co 7420  1c1 11201   + caddc 11203  5c5 12400  6c6 12401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

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

This theorem is used by:  8t8e64  12940  9t7e63  12946  5recm6rec  12964  fldiv4p1lem1div2  13975  s6len  15052  5ndvds6  16584  163prm  17303  631prm  17305  1259lem1  17309  1259lem4  17312  2503lem1  17315  2503lem2  17316  4001lem1  17319  4001lem4  17322  4001prm  17323  log2ublem3  27276  log2ub  27277  fib6  35038  hgt750lemd  35277  hgt750lem2  35281  60gcd7e1  43056  12lcm5e60  43059  3lexlogpow5ineq1  43105  3lexlogpow5ineq5  43111  aks4d1p1  43127  1p5e6  43313  3cubeslem3l  43697  fmtno5lem2  48639  fmtno5lem3  48640  fmtno5lem4  48641  fmtno4prmfac193  48658  fmtno4nprmfac193  48659  fmtno5faclem3  48666  flsqrt5  48679  127prm  48684  ppivalnnnprm  48713  gbowge7  48861  gbege6  48863  sbgoldbwt  48875  nnsum3primesle9  48892  veronesevrowd  50979  veroquadgsumlem  50983