| 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 12333 | . 2 ⊢ 6 = (5 + 1) | |
| 2 | 1 | eqcomi 2746 | 1 ⊢ (5 + 1) = 6 |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1540 (class class class)co 7431 1c1 11156 + caddc 11158 5c5 12324 6c6 12325 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-cleq 2729 df-6 12333 |
| This theorem is referenced by: 8t8e64 12854 9t7e63 12860 5recm6rec 12877 fldiv4p1lem1div2 13875 s6len 14940 5ndvds6 16451 163prm 17162 631prm 17164 1259lem1 17168 1259lem4 17171 2503lem1 17174 2503lem2 17175 4001lem1 17178 4001lem4 17181 4001prm 17182 log2ublem3 26991 log2ub 26992 fib6 34408 hgt750lemd 34663 hgt750lem2 34667 60gcd7e1 42006 12lcm5e60 42009 3lexlogpow5ineq1 42055 3lexlogpow5ineq5 42061 aks4d1p1 42077 3cubeslem3l 42697 fmtno5lem2 47541 fmtno5lem3 47542 fmtno5lem4 47543 fmtno4prmfac193 47560 fmtno4nprmfac193 47561 fmtno5faclem3 47568 flsqrt5 47581 127prm 47586 gbowge7 47750 gbege6 47752 sbgoldbwt 47764 nnsum3primesle9 47781 |
| Copyright terms: Public domain | W3C validator |