Theorem 5p1e6 12273

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

Syntax hints:   = wceq 1541  (class class class)co 7352  1c1 11013   + caddc 11015  5c5 12189  6c6 12190

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-6 12198

This theorem is referenced by:  8t8e64  12715  9t7e63  12721  5recm6rec  12737  fldiv4p1lem1div2  13745  s6len  14814  5ndvds6  16331  163prm  17042  631prm  17044  1259lem1  17048  1259lem4  17051  2503lem1  17054  2503lem2  17055  4001lem1  17058  4001lem4  17061  4001prm  17062  log2ublem3  26891  log2ub  26892  fib6  34426  hgt750lemd  34668  hgt750lem2  34672  60gcd7e1  42104  12lcm5e60  42107  3lexlogpow5ineq1  42153  3lexlogpow5ineq5  42159  aks4d1p1  42175  3cubeslem3l  42784  fmtno5lem2  47659  fmtno5lem3  47660  fmtno5lem4  47661  fmtno4prmfac193  47678  fmtno4nprmfac193  47679  fmtno5faclem3  47686  flsqrt5  47699  127prm  47704  gbowge7  47868  gbege6  47870  sbgoldbwt  47882  nnsum3primesle9  47899