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.
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?