Theorem 5p1e6 12270

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

Syntax hints:   = wceq 1540  (class class class)co 7349  1c1 11010   + caddc 11012  5c5 12186  6c6 12187

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 12195

This theorem is referenced by:  8t8e64  12712  9t7e63  12718  5recm6rec  12734  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  26856  log2ub  26857  fib6  34380  hgt750lemd  34622  hgt750lem2  34626  60gcd7e1  41988  12lcm5e60  41991  3lexlogpow5ineq1  42037  3lexlogpow5ineq5  42043  aks4d1p1  42059  3cubeslem3l  42669  fmtno5lem2  47548  fmtno5lem3  47549  fmtno5lem4  47550  fmtno4prmfac193  47567  fmtno4nprmfac193  47568  fmtno5faclem3  47575  flsqrt5  47588  127prm  47593  gbowge7  47757  gbege6  47759  sbgoldbwt  47771  nnsum3primesle9  47788