Theorem 5p1e6 12387

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

Syntax hints:   = wceq 1540  (class class class)co 7405  1c1 11130   + caddc 11132  5c5 12298  6c6 12299

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 2707

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

This theorem is referenced by:  8t8e64  12829  9t7e63  12835  5recm6rec  12851  fldiv4p1lem1div2  13852  s6len  14920  5ndvds6  16433  163prm  17144  631prm  17146  1259lem1  17150  1259lem4  17153  2503lem1  17156  2503lem2  17157  4001lem1  17160  4001lem4  17163  4001prm  17164  log2ublem3  26910  log2ub  26911  fib6  34438  hgt750lemd  34680  hgt750lem2  34684  60gcd7e1  42018  12lcm5e60  42021  3lexlogpow5ineq1  42067  3lexlogpow5ineq5  42073  aks4d1p1  42089  3cubeslem3l  42709  fmtno5lem2  47568  fmtno5lem3  47569  fmtno5lem4  47570  fmtno4prmfac193  47587  fmtno4nprmfac193  47588  fmtno5faclem3  47595  flsqrt5  47608  127prm  47613  gbowge7  47777  gbege6  47779  sbgoldbwt  47791  nnsum3primesle9  47808