![]() |
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 12219 | . 2 ⊢ 6 = (5 + 1) | |
2 | 1 | eqcomi 2745 | 1 ⊢ (5 + 1) = 6 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1541 (class class class)co 7356 1c1 11051 + caddc 11053 5c5 12210 6c6 12211 |
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-6 12219 |
This theorem is referenced by: 8t8e64 12738 9t7e63 12744 5recm6rec 12761 fldiv4p1lem1div2 13739 s6len 14789 163prm 16996 631prm 16998 1259lem1 17002 1259lem4 17005 2503lem1 17008 2503lem2 17009 4001lem1 17012 4001lem4 17015 4001prm 17016 log2ublem3 26296 log2ub 26297 fib6 32997 hgt750lemd 33252 hgt750lem2 33256 60gcd7e1 40453 12lcm5e60 40456 3lexlogpow5ineq1 40502 3lexlogpow5ineq5 40508 aks4d1p1 40524 3cubeslem3l 40987 fmtno5lem2 45718 fmtno5lem3 45719 fmtno5lem4 45720 fmtno4prmfac193 45737 fmtno4nprmfac193 45738 fmtno5faclem3 45745 flsqrt5 45758 127prm 45763 gbowge7 45927 gbege6 45929 sbgoldbwt 45941 nnsum3primesle9 45958 |
Copyright terms: Public domain | W3C validator |