Theorem 5p1e6 11155

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 11083	. 2 |- 6 = ( 5 + 1 )
2	1	eqcomi 2631	1 |- ( 5 + 1 ) = 6

Syntax hints:   = wceq 1483  (class class class)co 6650   1c1 9937   + caddc 9939   5c5 11073   6c6 11074

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-6 11083

This theorem is referenced by:  8t8e64  11662  9t7e63  11668  5recm6rec  11686  fldiv4p1lem1div2  12636  s6len  13646  163prm  15832  631prm  15834  prmo6  15837  1259lem1  15838  1259lem4  15841  2503lem1  15844  2503lem2  15845  4001lem1  15848  4001lem4  15851  4001prm  15852  log2ublem3  24675  log2ub  24676  fib6  30468  hgt750lemd  30726  hgt750lem2  30730  fmtno5lem2  41466  fmtno5lem3  41467  fmtno5lem4  41468  fmtno4prmfac193  41485  fmtno4nprmfac193  41486  fmtno5faclem3  41493  flsqrt5  41509  127prm  41515  gbowge7  41651  gbege6  41653  sbgoldbwt  41665  nnsum3primesle9  41682