According to Wikipedia's list of logic symbols:
A → B means A → B is false when A is true and B is false but true otherwise.
A ⊢ B means x ⊢ y means x proves (syntactically entails) y
But for me I can't see how they aren't equivalent. If a set of theorems/lemmas, A, can be used to derive another set of proofs/lemmas, B, then doesn't A imply B?
Googling around on this topic it seems that ⊢ may just be a "stronger" version of →. I know that we often use → for little steps in logic, and it seems that ⊢ is more used for larger steps.
Then I found this part of an answer in a question about symbol standardisation:
Now 'A implies B' gets used in informal talk both as variant on 'if A then B' and as a variant of 'A logically entails B', i.e. as both what we might regiment as → and as ⊢ [or ⊨]. And low and behold, we find ⟹ being confusingly used both ways [in the object language, or in the metalanguage]. Conservatism in symbolism is a Good Thing, so I think the use of ⟹ is to be deprecated: I'd say, use → for an object language conditional, and the appropriate turnstile in metalanguage.
(Emphasis mine)
So this would imply to me that → and ⊢ are equivalent, but it's idiomatic to use ⊢ for metamathematics, and → otherwise. Or, more concretely:
(A → B) → (C → D) is the same as (A → B) ⊢ (C → D), but the second option is considered more idiomatic/readable as we differentiate the smaller connections from the larger ones.
Is this right?
No, it means they are distinct application of a similar concept in different environments.
The reason the $\implies$ symbol is being depreciated, is because using the same symbol for these purposes is quite confusing.
A syntactic entailment means that when given a set of premises, the consequent may be derived using some specified set of axioms and rules of inference.