![]() |
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 11418 | . 2 ⊢ 6 = (5 + 1) | |
2 | 1 | eqcomi 2834 | 1 ⊢ (5 + 1) = 6 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1656 (class class class)co 6905 1c1 10253 + caddc 10255 5c5 11409 6c6 11410 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 ax-7 2112 ax-9 2173 ax-ext 2803 |
This theorem depends on definitions: df-bi 199 df-an 387 df-ex 1879 df-cleq 2818 df-6 11418 |
This theorem is referenced by: 8t8e64 11944 9t7e63 11950 5recm6rec 11967 fldiv4p1lem1div2 12931 s6len 14022 163prm 16197 631prm 16199 prmo6 16202 1259lem1 16203 1259lem4 16206 2503lem1 16209 2503lem2 16210 4001lem1 16213 4001lem4 16216 4001prm 16217 log2ublem3 25088 log2ub 25089 fib6 31003 hgt750lemd 31264 hgt750lem2 31268 fmtno5lem2 42289 fmtno5lem3 42290 fmtno5lem4 42291 fmtno4prmfac193 42308 fmtno4nprmfac193 42309 fmtno5faclem3 42316 flsqrt5 42332 127prm 42338 gbowge7 42474 gbege6 42476 sbgoldbwt 42488 nnsum3primesle9 42505 |
Copyright terms: Public domain | W3C validator |