Theorem 5p1e6 12405

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

Syntax hints:   = wceq 1534  (class class class)co 7416  1c1 11150   + caddc 11152  5c5 12316  6c6 12317

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-cleq 2718  df-6 12325

This theorem is referenced by:  8t8e64  12844  9t7e63  12850  5recm6rec  12867  fldiv4p1lem1div2  13849  s6len  14905  163prm  17122  631prm  17124  1259lem1  17128  1259lem4  17131  2503lem1  17134  2503lem2  17135  4001lem1  17138  4001lem4  17141  4001prm  17142  log2ublem3  26973  log2ub  26974  fib6  34253  hgt750lemd  34507  hgt750lem2  34511  60gcd7e1  41717  12lcm5e60  41720  3lexlogpow5ineq1  41766  3lexlogpow5ineq5  41772  aks4d1p1  41788  3cubeslem3l  42380  fmtno5lem2  47162  fmtno5lem3  47163  fmtno5lem4  47164  fmtno4prmfac193  47181  fmtno4nprmfac193  47182  fmtno5faclem3  47189  flsqrt5  47202  127prm  47207  gbowge7  47371  gbege6  47373  sbgoldbwt  47385  nnsum3primesle9  47402