Theorem 5p1e6 12411

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

Syntax hints:   = wceq 1537  (class class class)co 7431  1c1 11154   + caddc 11156  5c5 12322  6c6 12323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727  df-6 12331

This theorem is referenced by:  8t8e64  12852  9t7e63  12858  5recm6rec  12875  fldiv4p1lem1div2  13872  s6len  14937  5ndvds6  16448  163prm  17159  631prm  17161  1259lem1  17165  1259lem4  17168  2503lem1  17171  2503lem2  17172  4001lem1  17175  4001lem4  17178  4001prm  17179  log2ublem3  27006  log2ub  27007  fib6  34388  hgt750lemd  34642  hgt750lem2  34646  60gcd7e1  41987  12lcm5e60  41990  3lexlogpow5ineq1  42036  3lexlogpow5ineq5  42042  aks4d1p1  42058  3cubeslem3l  42674  fmtno5lem2  47479  fmtno5lem3  47480  fmtno5lem4  47481  fmtno4prmfac193  47498  fmtno4nprmfac193  47499  fmtno5faclem3  47506  flsqrt5  47519  127prm  47524  gbowge7  47688  gbege6  47690  sbgoldbwt  47702  nnsum3primesle9  47719