Theorem 5p1e6 12359

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

Syntax hints:   = wceq 1542  (class class class)co 7409  1c1 11111   + caddc 11113  5c5 12270  6c6 12271

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-6 12279

This theorem is referenced by:  8t8e64  12798  9t7e63  12804  5recm6rec  12821  fldiv4p1lem1div2  13800  s6len  14852  163prm  17058  631prm  17060  1259lem1  17064  1259lem4  17067  2503lem1  17070  2503lem2  17071  4001lem1  17074  4001lem4  17077  4001prm  17078  log2ublem3  26453  log2ub  26454  fib6  33405  hgt750lemd  33660  hgt750lem2  33664  60gcd7e1  40870  12lcm5e60  40873  3lexlogpow5ineq1  40919  3lexlogpow5ineq5  40925  aks4d1p1  40941  3cubeslem3l  41424  fmtno5lem2  46222  fmtno5lem3  46223  fmtno5lem4  46224  fmtno4prmfac193  46241  fmtno4nprmfac193  46242  fmtno5faclem3  46249  flsqrt5  46262  127prm  46267  gbowge7  46431  gbege6  46433  sbgoldbwt  46445  nnsum3primesle9  46462