![]() |
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 12220 | . 2 ⊢ 7 = (6 + 1) | |
2 | 1 | eqcomi 2745 | 1 ⊢ (6 + 1) = 7 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1541 (class class class)co 7356 1c1 11051 + caddc 11053 6c6 12211 7c7 12212 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-9 2116 ax-ext 2707 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1782 df-cleq 2728 df-7 12220 |
This theorem is referenced by: 9t8e72 12745 s7len 14790 37prm 16992 163prm 16996 317prm 16997 631prm 16998 1259lem1 17002 1259lem3 17004 1259lem4 17005 1259lem5 17006 2503lem1 17008 2503lem2 17009 2503lem3 17010 2503prm 17011 4001lem1 17012 4001lem4 17015 4001prm 17016 log2ublem3 26296 log2ub 26297 hgt750lemd 33201 hgt750lem2 33205 3exp7 40500 3lexlogpow5ineq1 40501 235t711 40782 ex-decpmul 40783 3cubeslem3l 40986 3cubeslem3r 40987 fmtno2 45713 fmtno3 45714 fmtno4 45715 fmtno5lem4 45719 fmtno5 45720 fmtno4nprmfac193 45737 fmtno5fac 45745 127prm 45762 mod42tp1mod8 45765 2exp340mod341 45896 gbowge7 45926 sbgoldbwt 45940 nnsum3primesle9 45957 |
Copyright terms: Public domain | W3C validator |