Theorem 5p1e6 11785

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

Syntax hints:   = wceq 1537  (class class class)co 7156  1c1 10538   + caddc 10540  5c5 11696  6c6 11697

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814  df-6 11705

This theorem is referenced by:  8t8e64  12220  9t7e63  12226  5recm6rec  12243  fldiv4p1lem1div2  13206  s6len  14263  163prm  16458  631prm  16460  1259lem1  16464  1259lem4  16467  2503lem1  16470  2503lem2  16471  4001lem1  16474  4001lem4  16477  4001prm  16478  log2ublem3  25526  log2ub  25527  fib6  31664  hgt750lemd  31919  hgt750lem2  31923  3cubeslem3l  39303  fmtno5lem2  43736  fmtno5lem3  43737  fmtno5lem4  43738  fmtno4prmfac193  43755  fmtno4nprmfac193  43756  fmtno5faclem3  43763  flsqrt5  43777  127prm  43783  gbowge7  43948  gbege6  43950  sbgoldbwt  43962  nnsum3primesle9  43979