Theorem 5p1e6 12267

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

Syntax hints:   = wceq 1541  (class class class)co 7346  1c1 11007   + caddc 11009  5c5 12183  6c6 12184

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-6 12192

This theorem is referenced by:  8t8e64  12709  9t7e63  12715  5recm6rec  12731  fldiv4p1lem1div2  13739  s6len  14808  5ndvds6  16325  163prm  17036  631prm  17038  1259lem1  17042  1259lem4  17045  2503lem1  17048  2503lem2  17049  4001lem1  17052  4001lem4  17055  4001prm  17056  log2ublem3  26885  log2ub  26886  fib6  34419  hgt750lemd  34661  hgt750lem2  34665  60gcd7e1  42097  12lcm5e60  42100  3lexlogpow5ineq1  42146  3lexlogpow5ineq5  42152  aks4d1p1  42168  3cubeslem3l  42778  fmtno5lem2  47653  fmtno5lem3  47654  fmtno5lem4  47655  fmtno4prmfac193  47672  fmtno4nprmfac193  47673  fmtno5faclem3  47680  flsqrt5  47693  127prm  47698  gbowge7  47862  gbege6  47864  sbgoldbwt  47876  nnsum3primesle9  47893