Theorem 5p1e6 12387

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

Syntax hints:   = wceq 1567  (class class class)co 7411  1c1 11101   + caddc 11103  5c5 12298  6c6 12299

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-6 12307

This theorem is referenced by:  8t8e64  12837  9t7e63  12843  5recm6rec  12861  fldiv4p1lem1div2  13868  s6len  14938  5ndvds6  16472  163prm  17185  631prm  17187  1259lem1  17191  1259lem4  17194  2503lem1  17197  2503lem2  17198  4001lem1  17201  4001lem4  17204  4001prm  17205  log2ublem3  27079  log2ub  27080  fib6  34741  hgt750lemd  34980  hgt750lem2  34984  60gcd7e1  42697  12lcm5e60  42700  3lexlogpow5ineq1  42746  3lexlogpow5ineq5  42752  aks4d1p1  42768  3cubeslem3l  43344  fmtno5lem2  48230  fmtno5lem3  48231  fmtno5lem4  48232  fmtno4prmfac193  48249  fmtno4nprmfac193  48250  fmtno5faclem3  48257  flsqrt5  48270  127prm  48275  ppivalnnnprm  48304  gbowge7  48452  gbege6  48454  sbgoldbwt  48466  nnsum3primesle9  48483