Theorem 5p1e6 12304

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

Syntax hints:   = wceq 1540  (class class class)co 7369  1c1 11045   + caddc 11047  5c5 12220  6c6 12221

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 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  8t8e64  12746  9t7e63  12752  5recm6rec  12768  fldiv4p1lem1div2  13773  s6len  14843  5ndvds6  16360  163prm  17071  631prm  17073  1259lem1  17077  1259lem4  17080  2503lem1  17083  2503lem2  17084  4001lem1  17087  4001lem4  17090  4001prm  17091  log2ublem3  26891  log2ub  26892  fib6  34390  hgt750lemd  34632  hgt750lem2  34636  60gcd7e1  41986  12lcm5e60  41989  3lexlogpow5ineq1  42035  3lexlogpow5ineq5  42041  aks4d1p1  42057  3cubeslem3l  42667  fmtno5lem2  47548  fmtno5lem3  47549  fmtno5lem4  47550  fmtno4prmfac193  47567  fmtno4nprmfac193  47568  fmtno5faclem3  47575  flsqrt5  47588  127prm  47593  gbowge7  47757  gbege6  47759  sbgoldbwt  47771  nnsum3primesle9  47788