Theorem 5p1e6 12289

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

Syntax hints:   = wceq 1542  (class class class)co 7358  1c1 11029   + caddc 11031  5c5 12205  6c6 12206

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2707

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

This theorem is referenced by:  8t8e64  12730  9t7e63  12736  5recm6rec  12752  fldiv4p1lem1div2  13757  s6len  14826  5ndvds6  16343  163prm  17054  631prm  17056  1259lem1  17060  1259lem4  17063  2503lem1  17066  2503lem2  17067  4001lem1  17070  4001lem4  17073  4001prm  17074  log2ublem3  26916  log2ub  26917  fib6  34542  hgt750lemd  34784  hgt750lem2  34788  60gcd7e1  42294  12lcm5e60  42297  3lexlogpow5ineq1  42343  3lexlogpow5ineq5  42349  aks4d1p1  42365  3cubeslem3l  42965  fmtno5lem2  47837  fmtno5lem3  47838  fmtno5lem4  47839  fmtno4prmfac193  47856  fmtno4nprmfac193  47857  fmtno5faclem3  47864  flsqrt5  47877  127prm  47882  gbowge7  48046  gbege6  48048  sbgoldbwt  48060  nnsum3primesle9  48077