Eiffel has Implication
It actually has even more. It has a number of semi-strict operators as well as strict.
The reason programmers do not use such things is because they are never trained to know precisely what they are, how to use them, and when to use them -- as well as how to design with them. Because they are never trained, they never ask for it from the compiler writers, which is why the compiler people do not bother putting such mechanisms in the compiler. When Computer Science students and Shade-tree programmers begin getting a more rounded education, then the compilers will start catching up.
It turns out that once you have a language with such Boolean operators and you know how to design with them and use them, then you use them.
In Eiffel the use of the "implies" keyword is rather prominent because of Design-by-Contract due to the Boolean-heavy nature of contract assertions. There are some contracts that can only be written properly and efficiently with the "implies" operator. This then begs the comment that languages without contracts are further without cause to look at, train, and implement the use of implication.
Add to this that most programmers are "math-and-logic-weak" tells us the remainder of the story. Even if you are math-and-logic-heavy in your education, when one chooses a language that does not implement constructs such as implication, then one tends to think such things are unnecessary or not useful. One rarely questions the language and gets into an echo-chamber of: "Well the compiler guys don't see the need" and "Well the programmers don't see the need" -- endless and vicious circle.
Instead, the compiler people need to back up to the theory, write a language notation that is suggested or implied by the theory (e.g. Object Oriented Theory) regardless of what the unwashed masses of programmers think or ask for. From there, professors, teachers, and other professionals need to expertly train young mush-minds based on raw theory and NOT "theory-through-the-language-lens". When this happens, people will suddenly wake up and realize what they have been missing and what has been foisted on them.
Right now -- there is so much theory out there that masquerades as Object Oriented, but is just O-O-through-a-glass-darkly-of-[pick-your-language]. One cannot read most "theory" books on O-O because they want to interpret what the theory is through the lens of some language. Totally false and incorrect. It would be like teaching math-based-on-my-calculator or my slide rule. NO -- one allows reality to teach one about itself and then uses a notation to describe what one observes -- that's called "science". This other mash called O-O-based-on-language-X is so skewed as to barely represent reality.
So, step away from the language, take a look at raw theory, and begin again. Do not let limitations, constraints, and paint-jobs of a language tell you what the theory is. Simply let the reality of the theory dictate its own notation and then move from there into formulating a language.
From there, you will start to get how implication and "implies" is not only useful, but elegant and very cool!
Have a great one!