Theorem 5p1e6 11787

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

Syntax hints:   = wceq 1536  (class class class)co 7159  1c1 10541   + caddc 10543  5c5 11698  6c6 11699

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-9 2123  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1780  df-cleq 2817  df-6 11707

This theorem is referenced by:  8t8e64  12222  9t7e63  12228  5recm6rec  12245  fldiv4p1lem1div2  13208  s6len  14266  163prm  16461  631prm  16463  1259lem1  16467  1259lem4  16470  2503lem1  16473  2503lem2  16474  4001lem1  16477  4001lem4  16480  4001prm  16481  log2ublem3  25529  log2ub  25530  fib6  31668  hgt750lemd  31923  hgt750lem2  31927  3cubeslem3l  39289  fmtno5lem2  43723  fmtno5lem3  43724  fmtno5lem4  43725  fmtno4prmfac193  43742  fmtno4nprmfac193  43743  fmtno5faclem3  43750  flsqrt5  43764  127prm  43770  gbowge7  43935  gbege6  43937  sbgoldbwt  43949  nnsum3primesle9  43966