You are absolutely and 100% correct. In the language of the Logical Calculus, my four statements are a verbose version of both manav's two statements and your one statement. However, most people, including most programmers, do not know the Logical Calculus. Coupled with the fact that logic expressed within natural language does not conform to the Logical Calculus and you can see why I would feel compelled to clarify manav's statements.

To further clarify, "implies" has both a formal and an informal definition. The formal definition is as you say. The informal definition for implies is much closer to "if and only if" than "if-then", manav's second statement nothwithstanding. Because the converse is implied when using "implies", I felt the need to explicate the four truth-possibilities, so that there would be no misunderstanding.