![]() |
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 12229 | . 2 ⊢ 6 = (5 + 1) | |
2 | 1 | eqcomi 2740 | 1 ⊢ (5 + 1) = 6 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1541 (class class class)co 7362 1c1 11061 + caddc 11063 5c5 12220 6c6 12221 |
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 2702 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1782 df-cleq 2723 df-6 12229 |
This theorem is referenced by: 8t8e64 12748 9t7e63 12754 5recm6rec 12771 fldiv4p1lem1div2 13750 s6len 14802 163prm 17008 631prm 17010 1259lem1 17014 1259lem4 17017 2503lem1 17020 2503lem2 17021 4001lem1 17024 4001lem4 17027 4001prm 17028 log2ublem3 26335 log2ub 26336 fib6 33095 hgt750lemd 33350 hgt750lem2 33354 60gcd7e1 40535 12lcm5e60 40538 3lexlogpow5ineq1 40584 3lexlogpow5ineq5 40590 aks4d1p1 40606 3cubeslem3l 41067 fmtno5lem2 45866 fmtno5lem3 45867 fmtno5lem4 45868 fmtno4prmfac193 45885 fmtno4nprmfac193 45886 fmtno5faclem3 45893 flsqrt5 45906 127prm 45911 gbowge7 46075 gbege6 46077 sbgoldbwt 46089 nnsum3primesle9 46106 |
Copyright terms: Public domain | W3C validator |