Verify the following rules and explain these rules in natural language:

1 x ∧ (x → y) → y modus ponens;

2 y ∧ (x → y) → x modus tollens;

3 (x → y) → (y → x) contrapositive;

4 (x → y) ∧ (y → z) → (x → z) hypothetical syllogism;