Theorem 5p1e6 12335

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

Syntax hints:   = wceq 1540  (class class class)co 7390  1c1 11076   + caddc 11078  5c5 12251  6c6 12252

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 2702

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

This theorem is referenced by:  8t8e64  12777  9t7e63  12783  5recm6rec  12799  fldiv4p1lem1div2  13804  s6len  14874  5ndvds6  16391  163prm  17102  631prm  17104  1259lem1  17108  1259lem4  17111  2503lem1  17114  2503lem2  17115  4001lem1  17118  4001lem4  17121  4001prm  17122  log2ublem3  26865  log2ub  26866  fib6  34404  hgt750lemd  34646  hgt750lem2  34650  60gcd7e1  42000  12lcm5e60  42003  3lexlogpow5ineq1  42049  3lexlogpow5ineq5  42055  aks4d1p1  42071  3cubeslem3l  42681  fmtno5lem2  47559  fmtno5lem3  47560  fmtno5lem4  47561  fmtno4prmfac193  47578  fmtno4nprmfac193  47579  fmtno5faclem3  47586  flsqrt5  47599  127prm  47604  gbowge7  47768  gbege6  47770  sbgoldbwt  47782  nnsum3primesle9  47799