Theorem 5p1e6 12318

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

Syntax hints:   = wceq 1548  (class class class)co 7360  1c1 11034   + caddc 11036  5c5 12234  6c6 12235

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 1975  ax-7 2016  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-cleq 2733  df-6 12243

This theorem is referenced by:  8t8e64  12760  9t7e63  12766  5recm6rec  12782  fldiv4p1lem1div2  13789  s6len  14858  5ndvds6  16378  163prm  17090  631prm  17092  1259lem1  17096  1259lem4  17099  2503lem1  17102  2503lem2  17103  4001lem1  17106  4001lem4  17109  4001prm  17110  log2ublem3  26934  log2ub  26935  fib6  34602  hgt750lemd  34844  hgt750lem2  34848  60gcd7e1  42505  12lcm5e60  42508  3lexlogpow5ineq1  42554  3lexlogpow5ineq5  42560  aks4d1p1  42576  3cubeslem3l  43150  fmtno5lem2  48046  fmtno5lem3  48047  fmtno5lem4  48048  fmtno4prmfac193  48065  fmtno4nprmfac193  48066  fmtno5faclem3  48073  flsqrt5  48086  127prm  48091  ppivalnnnprm  48120  gbowge7  48268  gbege6  48270  sbgoldbwt  48282  nnsum3primesle9  48299