Theorem 5p1e6 12025

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

Syntax hints:   = wceq 1543  (class class class)co 7252  1c1 10778   + caddc 10780  5c5 11936  6c6 11937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-9 2122  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2731  df-6 11945

This theorem is referenced by:  8t8e64  12462  9t7e63  12468  5recm6rec  12485  fldiv4p1lem1div2  13458  s6len  14517  163prm  16729  631prm  16731  1259lem1  16735  1259lem4  16738  2503lem1  16741  2503lem2  16742  4001lem1  16745  4001lem4  16748  4001prm  16749  log2ublem3  25978  log2ub  25979  fib6  32248  hgt750lemd  32503  hgt750lem2  32507  60gcd7e1  39920  12lcm5e60  39923  3lexlogpow5ineq1  39969  3lexlogpow5ineq5  39975  aks4d1p1  39990  3cubeslem3l  40396  fmtno5lem2  44867  fmtno5lem3  44868  fmtno5lem4  44869  fmtno4prmfac193  44886  fmtno4nprmfac193  44887  fmtno5faclem3  44894  flsqrt5  44907  127prm  44912  gbowge7  45076  gbege6  45078  sbgoldbwt  45090  nnsum3primesle9  45107