Theorem 5p1e6 12309

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 2740	1 ⊢ (5 + 1) = 6

Syntax hints:   = wceq 1541  (class class class)co 7362  1c1 11061   + caddc 11063  5c5 12220  6c6 12221

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723  df-6 12229

This theorem is referenced by:  8t8e64  12748  9t7e63  12754  5recm6rec  12771  fldiv4p1lem1div2  13750  s6len  14802  163prm  17008  631prm  17010  1259lem1  17014  1259lem4  17017  2503lem1  17020  2503lem2  17021  4001lem1  17024  4001lem4  17027  4001prm  17028  log2ublem3  26335  log2ub  26336  fib6  33095  hgt750lemd  33350  hgt750lem2  33354  60gcd7e1  40535  12lcm5e60  40538  3lexlogpow5ineq1  40584  3lexlogpow5ineq5  40590  aks4d1p1  40606  3cubeslem3l  41067  fmtno5lem2  45866  fmtno5lem3  45867  fmtno5lem4  45868  fmtno4prmfac193  45885  fmtno4nprmfac193  45886  fmtno5faclem3  45893  flsqrt5  45906  127prm  45911  gbowge7  46075  gbege6  46077  sbgoldbwt  46089  nnsum3primesle9  46106