Theorem 5p1e6 12414

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

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7416  1c1 11128   + caddc 11130  5c5 12325  6c6 12326

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754  df-6 12334

This theorem is used by:  8t8e64  12865  9t7e63  12871  5recm6rec  12889  fldiv4p1lem1div2  13898  s6len  14974  5ndvds6  16508  163prm  17221  631prm  17223  1259lem1  17227  1259lem4  17230  2503lem1  17233  2503lem2  17234  4001lem1  17237  4001lem4  17240  4001prm  17241  log2ublem3  27183  log2ub  27184  fib6  34904  hgt750lemd  35143  hgt750lem2  35147  60gcd7e1  42858  12lcm5e60  42861  3lexlogpow5ineq1  42907  3lexlogpow5ineq5  42913  aks4d1p1  42929  1p5e6  43115  3cubeslem3l  43518  fmtno5lem2  48444  fmtno5lem3  48445  fmtno5lem4  48446  fmtno4prmfac193  48463  fmtno4nprmfac193  48464  fmtno5faclem3  48471  flsqrt5  48484  127prm  48489  ppivalnnnprm  48518  gbowge7  48666  gbege6  48668  sbgoldbwt  48680  nnsum3primesle9  48697  veronesevrowd  50799  veroquadgsumlem  50803