![]() |
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 12325 | . 2 ⊢ 6 = (5 + 1) | |
2 | 1 | eqcomi 2735 | 1 ⊢ (5 + 1) = 6 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1534 (class class class)co 7416 1c1 11150 + caddc 11152 5c5 12316 6c6 12317 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1775 df-cleq 2718 df-6 12325 |
This theorem is referenced by: 8t8e64 12844 9t7e63 12850 5recm6rec 12867 fldiv4p1lem1div2 13849 s6len 14905 163prm 17122 631prm 17124 1259lem1 17128 1259lem4 17131 2503lem1 17134 2503lem2 17135 4001lem1 17138 4001lem4 17141 4001prm 17142 log2ublem3 26973 log2ub 26974 fib6 34253 hgt750lemd 34507 hgt750lem2 34511 60gcd7e1 41717 12lcm5e60 41720 3lexlogpow5ineq1 41766 3lexlogpow5ineq5 41772 aks4d1p1 41788 3cubeslem3l 42380 fmtno5lem2 47162 fmtno5lem3 47163 fmtno5lem4 47164 fmtno4prmfac193 47181 fmtno4nprmfac193 47182 fmtno5faclem3 47189 flsqrt5 47202 127prm 47207 gbowge7 47371 gbege6 47373 sbgoldbwt 47385 nnsum3primesle9 47402 |
Copyright terms: Public domain | W3C validator |