I have problem with understanding why precondition strengthening is sound rule in Hoare logic. The rule is:
$$ {P \implies Q, \{Q\} C \{X\} } \over {\{P\} C \{X\}} $$
I really do not understand why precondition in consequence goes in reverse direction that implication works (modus ponens).
I can understand why post-condition weakening works because it follows modus ponens rule but I am no able to understand precondition strengthening.