Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 5p1e6 | Structured version Visualization version GIF version |
Description: 5 + 1 = 6. (Contributed by Mario Carneiro, 18-Apr-2015.) |
Ref | Expression |
---|---|
5p1e6 | ⊢ (5 + 1) = 6 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-6 11693 | . 2 ⊢ 6 = (5 + 1) | |
2 | 1 | eqcomi 2830 | 1 ⊢ (5 + 1) = 6 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1528 (class class class)co 7145 1c1 10527 + caddc 10529 5c5 11684 6c6 11685 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-9 2115 ax-ext 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-cleq 2814 df-6 11693 |
This theorem is referenced by: 8t8e64 12208 9t7e63 12214 5recm6rec 12231 fldiv4p1lem1div2 13195 s6len 14253 163prm 16448 631prm 16450 1259lem1 16454 1259lem4 16457 2503lem1 16460 2503lem2 16461 4001lem1 16464 4001lem4 16467 4001prm 16468 log2ublem3 25454 log2ub 25455 fib6 31564 hgt750lemd 31819 hgt750lem2 31823 3cubeslem3l 39163 fmtno5lem2 43563 fmtno5lem3 43564 fmtno5lem4 43565 fmtno4prmfac193 43582 fmtno4nprmfac193 43583 fmtno5faclem3 43590 flsqrt5 43604 127prm 43610 gbowge7 43775 gbege6 43777 sbgoldbwt 43789 nnsum3primesle9 43806 |
Copyright terms: Public domain | W3C validator |