Theorem 5p1e6 11772

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

Syntax hints:   = wceq 1538  (class class class)co 7135  1c1 10527   + caddc 10529  5c5 11683  6c6 11684

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-6 11692

This theorem is referenced by:  8t8e64  12207  9t7e63  12213  5recm6rec  12230  fldiv4p1lem1div2  13200  s6len  14254  163prm  16450  631prm  16452  1259lem1  16456  1259lem4  16459  2503lem1  16462  2503lem2  16463  4001lem1  16466  4001lem4  16469  4001prm  16470  log2ublem3  25534  log2ub  25535  fib6  31774  hgt750lemd  32029  hgt750lem2  32033  60gcd7e1  39293  12lcm5e60  39296  3cubeslem3l  39627  fmtno5lem2  44071  fmtno5lem3  44072  fmtno5lem4  44073  fmtno4prmfac193  44090  fmtno4nprmfac193  44091  fmtno5faclem3  44098  flsqrt5  44111  127prm  44116  gbowge7  44281  gbege6  44283  sbgoldbwt  44295  nnsum3primesle9  44312