Theorem 5p1e6 12323

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

Syntax hints:   = wceq 1542  (class class class)co 7367  1c1 11039   + caddc 11041  5c5 12239  6c6 12240

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 2708

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

This theorem is referenced by:  8t8e64  12765  9t7e63  12771  5recm6rec  12787  fldiv4p1lem1div2  13794  s6len  14863  5ndvds6  16383  163prm  17095  631prm  17097  1259lem1  17101  1259lem4  17104  2503lem1  17107  2503lem2  17108  4001lem1  17111  4001lem4  17114  4001prm  17115  log2ublem3  26912  log2ub  26913  fib6  34550  hgt750lemd  34792  hgt750lem2  34796  60gcd7e1  42444  12lcm5e60  42447  3lexlogpow5ineq1  42493  3lexlogpow5ineq5  42499  aks4d1p1  42515  3cubeslem3l  43118  fmtno5lem2  48017  fmtno5lem3  48018  fmtno5lem4  48019  fmtno4prmfac193  48036  fmtno4nprmfac193  48037  fmtno5faclem3  48044  flsqrt5  48057  127prm  48062  ppivalnnnprm  48091  gbowge7  48239  gbege6  48241  sbgoldbwt  48253  nnsum3primesle9  48270