Theorem 5p1e6 12366

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

Syntax hints:   = wceq 1562  (class class class)co 7398  1c1 11076   + caddc 11078  5c5 12277  6c6 12278

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1802  df-cleq 2756  df-6 12286

This theorem is referenced by:  8t8e64  12816  9t7e63  12822  5recm6rec  12840  fldiv4p1lem1div2  13847  s6len  14916  5ndvds6  16450  163prm  17163  631prm  17165  1259lem1  17169  1259lem4  17172  2503lem1  17175  2503lem2  17176  4001lem1  17179  4001lem4  17182  4001prm  17183  log2ublem3  27015  log2ub  27016  fib6  34705  hgt750lemd  34944  hgt750lem2  34948  60gcd7e1  42627  12lcm5e60  42630  3lexlogpow5ineq1  42676  3lexlogpow5ineq5  42682  aks4d1p1  42698  3cubeslem3l  43272  fmtno5lem2  48168  fmtno5lem3  48169  fmtno5lem4  48170  fmtno4prmfac193  48187  fmtno4nprmfac193  48188  fmtno5faclem3  48195  flsqrt5  48208  127prm  48213  ppivalnnnprm  48242  gbowge7  48390  gbege6  48392  sbgoldbwt  48404  nnsum3primesle9  48421