Theorem 5p1e6 11505

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

Syntax hints:   = wceq 1656  (class class class)co 6905  1c1 10253   + caddc 10255  5c5 11409  6c6 11410

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1879  df-cleq 2818  df-6 11418

This theorem is referenced by:  8t8e64  11944  9t7e63  11950  5recm6rec  11967  fldiv4p1lem1div2  12931  s6len  14022  163prm  16197  631prm  16199  prmo6  16202  1259lem1  16203  1259lem4  16206  2503lem1  16209  2503lem2  16210  4001lem1  16213  4001lem4  16216  4001prm  16217  log2ublem3  25088  log2ub  25089  fib6  31003  hgt750lemd  31264  hgt750lem2  31268  fmtno5lem2  42289  fmtno5lem3  42290  fmtno5lem4  42291  fmtno4prmfac193  42308  fmtno4nprmfac193  42309  fmtno5faclem3  42316  flsqrt5  42332  127prm  42338  gbowge7  42474  gbege6  42476  sbgoldbwt  42488  nnsum3primesle9  42505