Theorem 5p1e6 12440

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

Syntax hints:   = wceq 1537  (class class class)co 7448  1c1 11185   + caddc 11187  5c5 12351  6c6 12352

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-6 12360

This theorem is referenced by:  8t8e64  12879  9t7e63  12885  5recm6rec  12902  fldiv4p1lem1div2  13886  s6len  14950  163prm  17172  631prm  17174  1259lem1  17178  1259lem4  17181  2503lem1  17184  2503lem2  17185  4001lem1  17188  4001lem4  17191  4001prm  17192  log2ublem3  27009  log2ub  27010  fib6  34371  hgt750lemd  34625  hgt750lem2  34629  60gcd7e1  41962  12lcm5e60  41965  3lexlogpow5ineq1  42011  3lexlogpow5ineq5  42017  aks4d1p1  42033  3cubeslem3l  42642  fmtno5lem2  47428  fmtno5lem3  47429  fmtno5lem4  47430  fmtno4prmfac193  47447  fmtno4nprmfac193  47448  fmtno5faclem3  47455  flsqrt5  47468  127prm  47473  gbowge7  47637  gbege6  47639  sbgoldbwt  47651  nnsum3primesle9  47668