Theorem 5p1e6 12413

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

Syntax hints:   = wceq 1540  (class class class)co 7431  1c1 11156   + caddc 11158  5c5 12324  6c6 12325

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-6 12333

This theorem is referenced by:  8t8e64  12854  9t7e63  12860  5recm6rec  12877  fldiv4p1lem1div2  13875  s6len  14940  5ndvds6  16451  163prm  17162  631prm  17164  1259lem1  17168  1259lem4  17171  2503lem1  17174  2503lem2  17175  4001lem1  17178  4001lem4  17181  4001prm  17182  log2ublem3  26991  log2ub  26992  fib6  34408  hgt750lemd  34663  hgt750lem2  34667  60gcd7e1  42006  12lcm5e60  42009  3lexlogpow5ineq1  42055  3lexlogpow5ineq5  42061  aks4d1p1  42077  3cubeslem3l  42697  fmtno5lem2  47541  fmtno5lem3  47542  fmtno5lem4  47543  fmtno4prmfac193  47560  fmtno4nprmfac193  47561  fmtno5faclem3  47568  flsqrt5  47581  127prm  47586  gbowge7  47750  gbege6  47752  sbgoldbwt  47764  nnsum3primesle9  47781