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 11895 | . 2 ⊢ 7 = (6 + 1) | |
2 | 1 | eqcomi 2746 | 1 ⊢ (6 + 1) = 7 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1543 (class class class)co 7210 1c1 10727 + caddc 10729 6c6 11886 7c7 11887 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-9 2120 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1788 df-cleq 2729 df-7 11895 |
This theorem is referenced by: 9t8e72 12418 s7len 14464 37prm 16671 163prm 16675 317prm 16676 631prm 16677 1259lem1 16681 1259lem3 16683 1259lem4 16684 1259lem5 16685 2503lem1 16687 2503lem2 16688 2503lem3 16689 2503prm 16690 4001lem1 16691 4001lem4 16694 4001prm 16695 log2ublem3 25828 log2ub 25829 hgt750lemd 32337 hgt750lem2 32341 3exp7 39793 3lexlogpow5ineq1 39794 235t711 40024 ex-decpmul 40025 3cubeslem3l 40209 3cubeslem3r 40210 fmtno2 44673 fmtno3 44674 fmtno4 44675 fmtno5lem4 44679 fmtno5 44680 fmtno4nprmfac193 44697 fmtno5fac 44705 127prm 44722 mod42tp1mod8 44725 2exp340mod341 44856 gbowge7 44886 sbgoldbwt 44900 nnsum3primesle9 44917 |
Copyright terms: Public domain | W3C validator |