![]() |
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 11377 | . 2 ⊢ 7 = (6 + 1) | |
2 | 1 | eqcomi 2806 | 1 ⊢ (6 + 1) = 7 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1653 (class class class)co 6876 1c1 10223 + caddc 10225 6c6 11368 7c7 11369 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-ext 2775 |
This theorem depends on definitions: df-bi 199 df-an 386 df-ex 1876 df-cleq 2790 df-7 11377 |
This theorem is referenced by: 9t8e72 11909 s7len 13984 37prm 16152 163prm 16156 317prm 16157 631prm 16158 1259lem1 16162 1259lem3 16164 1259lem4 16165 1259lem5 16166 2503lem1 16168 2503lem2 16169 2503lem3 16170 2503prm 16171 4001lem1 16172 4001lem4 16175 4001prm 16176 log2ublem3 25024 log2ub 25025 hgt750lemd 31238 hgt750lem2 31242 235t711 37992 ex-decpmul 37993 fmtno2 42232 fmtno3 42233 fmtno4 42234 fmtno5lem4 42238 fmtno5 42239 fmtno4nprmfac193 42256 fmtno5fac 42264 127prm 42285 mod42tp1mod8 42289 gbowge7 42421 sbgoldbwt 42435 nnsum3primesle9 42452 |
Copyright terms: Public domain | W3C validator |