| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > 6p1e7 | Structured version Visualization version GIF version | ||
| Description: 6 + 1 = 7. (Contributed by Mario Carneiro, 18-Apr-2015.) |
| Ref | Expression |
|---|---|
| 6p1e7 | ⊢ (6 + 1) = 7 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-7 12285 | . 2 ⊢ 7 = (6 + 1) | |
| 2 | 1 | eqcomi 2771 | 1 ⊢ (6 + 1) = 7 |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1560 (class class class)co 7396 1c1 11074 + caddc 11076 6c6 12276 7c7 12277 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1815 ax-4 1829 ax-5 1930 ax-6 1987 ax-7 2028 ax-9 2152 ax-ext 2734 |
| This theorem depends on definitions: df-bi 209 df-an 400 df-ex 1800 df-cleq 2754 df-7 12285 |
| This theorem is referenced by: 9t8e72 12821 s7len 14915 37prm 17157 163prm 17161 317prm 17162 631prm 17163 1259lem1 17167 1259lem3 17169 1259lem4 17170 1259lem5 17171 2503lem1 17173 2503lem2 17174 2503lem3 17175 2503prm 17176 4001lem1 17177 4001lem4 17180 4001prm 17181 log2ublem3 27013 log2ub 27014 hgt750lemd 34942 hgt750lem2 34946 3exp7 42670 3lexlogpow5ineq1 42671 235t711 42914 ex-decpmul 42915 3cubeslem3l 43267 3cubeslem3r 43268 fmtno2 48159 fmtno3 48160 fmtno4 48161 fmtno5lem4 48165 fmtno5 48166 fmtno4nprmfac193 48183 fmtno5fac 48191 127prm 48208 mod42tp1mod8 48211 ppivalnn4 48236 2exp340mod341 48355 gbowge7 48385 sbgoldbwt 48399 nnsum3primesle9 48416 |
| Copyright terms: Public domain | W3C validator |