![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 5p1e6 | Structured version Visualization version Unicode version |
Description: 5 + 1 = 6. (Contributed by Mario Carneiro, 18-Apr-2015.) |
Ref | Expression |
---|---|
5p1e6 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-6 10672 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | eqcomi 2460 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-ext 2431 |
This theorem depends on definitions: df-bi 189 df-cleq 2444 df-6 10672 |
This theorem is referenced by: 8t8e64 11145 9t7e63 11151 5recm6rec 11158 s6len 12995 2exp6OLD 15059 163prm 15096 631prm 15098 prmo6 15101 1259lem1 15102 1259lem3 15104 1259lem4 15105 2503lem1 15108 2503lem2 15109 4001lem1 15112 4001lem4 15115 4001prm 15116 log2ublem3 23874 log2ub 23875 fib6 29239 gboge7 38864 gbege6 38866 bgoldbwt 38878 nnsum3primesle9 38889 |
Copyright terms: Public domain | W3C validator |