Theorem 5p1e6 12328

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

Syntax hints:   = wceq 1540  (class class class)co 7387  1c1 11069   + caddc 11071  5c5 12244  6c6 12245

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-6 12253

This theorem is referenced by:  8t8e64  12770  9t7e63  12776  5recm6rec  12792  fldiv4p1lem1div2  13797  s6len  14867  5ndvds6  16384  163prm  17095  631prm  17097  1259lem1  17101  1259lem4  17104  2503lem1  17107  2503lem2  17108  4001lem1  17111  4001lem4  17114  4001prm  17115  log2ublem3  26858  log2ub  26859  fib6  34397  hgt750lemd  34639  hgt750lem2  34643  60gcd7e1  41993  12lcm5e60  41996  3lexlogpow5ineq1  42042  3lexlogpow5ineq5  42048  aks4d1p1  42064  3cubeslem3l  42674  fmtno5lem2  47555  fmtno5lem3  47556  fmtno5lem4  47557  fmtno4prmfac193  47574  fmtno4nprmfac193  47575  fmtno5faclem3  47582  flsqrt5  47595  127prm  47600  gbowge7  47764  gbege6  47766  sbgoldbwt  47778  nnsum3primesle9  47795