The $\to$ is indeed used for material implication: it is a logical operator and combines two logic expression into a larger logic expression. It has a semantics as provided by its truth-table, that I am sure you are familiar with.
On the other hand, the $\Rightarrow$ is typically used for logical implication. This symbol is a meta-logical symbol. It does not combine two logic statements into one larger logic statement, and it does not have a truth-table. Rather, it says something about those two logic statements. $P1 \Rightarrow P2$ says that $P2$ is a logical consequence of $P1$: that it is impossible for $P1$ to be true and $P2$ to be false at the same time.
Example: $P \land Q \Rightarrow P$ is true, since it is impossible for $P \land Q$ to be true but $P$ to be false. On the other hand we do not have that $P \Rightarrow Q$: it is possible for $P$ to be true and $Q$ to be false. How is this different from $P \to Q$? Well, I could symbolize: 'If there is smoke, then there is fire' with $P \to Q$ ... so that would be my way of saying that in the particular world I am trying to describe, $P \to Q$ is true. But, since there are also logically possible worlds where you can have smoke without fire, we do not have that $P \Rightarrow Q$
Sometimes we use $P \vDash Q$ to represent the same logical implication relationship ... though we often use $\vDash$ using sets of statements. So, with your example, we could say:
$$\{ P1 \to P2, P2 \to P3 \} \vDash P1 \to P3$$
though we can conjunct the statements from the implying set of statements into a single statement, and thus say:
$$( P1 \to P2) \land (P2 \to P3) \Rightarrow P1 \to P3$$
Now, here is an interesting relationship between $\to$ and $\Rightarrow$: $P1 \Rightarrow P2$ is true if and only if $P1 \to P2$ is a logical tautology (i.e. always true when evaluated on a truth-table). So, for the above example, we can say that $$(( P1 \to P2) \land (P2 \to P3)) \to (P1 \to P3)$$ is a logical tautology. By the way, we can write $\Rightarrow P$ or $\vDash P$ to indicate that $P$ is a tautology, i.e. we have:
$$P1 \Rightarrow P2 \text{ if and only if } \Rightarrow (P1 \to P2)$$
Of course, you can take any fact of logical consequence, and turn it into an inference rule. Thus, we can indeed say that:
$$P1 \to P2$$
$$P2 \to P3$$
$$ \therefore P1 \to P3$$
is an inference rule, and many textbooks do exactly that, calling it Hypothetical Syllogism or Chain Argument. To indicate it is a rule of inference for some formal proof system, though, we typically use the $\vdash$ symbol. In this case, we would say:
$$P1 \to P2, P2 \to P3 \vdash P1 \to P3$$
or
$$\{ P1 \to P2, P2 \to P3 \} \vdash P1 \to P3$$
Perversely, you can define anything an inference rule. If I wanted to, I could say that:
$$P$$
$$\therefore P \land Q$$
is an inference rule, and call it "Modus Bogus"
I would thus write $$P \vdash P \land Q$$
Note that of course this is not a valid inference rule, because it is not true that $$P \vDash P \land Q$$
Finally, the three formulas at the bottom of your post could be seen as single logic formulas, if we treat the $\equiv$ as the symbol for the material biconditional operator. As such, they would all be tautologies. But, most likely they are used as logical equivalence symbols, i.e. as meta-logical symbols that state that the statement on the left is logically equivalent to the statement on the right. For this, however, we typically use $\Leftrightarrow$
Some further connections: We have that for any statements $P1$ and $P2$:
$$P1 \leftrightarrow P2 \Leftrightarrow (P1 \to P2) \land (P2 \to P1)$$
and thus also that:
$$\Rightarrow (P1 \leftrightarrow P2) \leftrightarrow ((P1 \to P2) \land (P2 \to P1))$$
And as a really nice mix up of three different uses of 'if and only if', we have:
$$P1 \Leftrightarrow P2 \text{ if and only if } \Rightarrow P1 \leftrightarrow P2$$
So yes, it is all pretty confusing, and to make matters worse, there is no strict standard on the use of these symbols: some textbooks use $\Rightarrow$ for the material conditional/implication, while others use it for the logical implication. Likewise, some textbooks use $\Leftrightarrow$ for the material biconditional, while others use it for the logical equivalence. And, some textbooks use $\equiv$ for the material biconditional, while others use it for the logical equivalence.
Best Answer
The truth-function conditional, also called the material conditional, is a binary boolean truth function whose values are as you described in the truth table; it is true for all inputs except when the antecedent (left hand side) is true and the consequent (right hand side) is false. The conditional is written with a variety of symbols, e.g., $P \to Q$, $P \supset Q$, and $P \Rightarrow Q$.
There is an inference rule called modus ponens which says that from a conditional $P \to Q$ and $P$, infer $Q$. This can be written in a number of ways, e.g.,
or
$$ \begin{array}{c} P \quad P \to Q \\ \hline Q \end{array} $$
Because modus ponens is so important, and because in some axiomatic systems it is the only inference rule, it is sometimes called “the inference rule.” Most of the time, that usage should probably be avoided, because in practice (i.e., outside of those specific axiomatic systems), there are plenty of other inference rules, and modus ponens is just one among many.
Asserting that the conditional $P \to Q$ is true is simply to assert that either:
Using the inference rule modus ponens lets us affirm that $Q$ is true, based on the prior assertion that $P \to Q$ is true and that $P$ is true.
Modus ponens is a sound inference rule because whenever all the premises are actually true, then the conclusion is also actually true. To see why this is the case, consider the premises to modus ponens. These are a conditional $P \to Q$ and $P$. If $P \to Q$ is true, then one of the three cases (a, b, c) described above must also be true. $P \to Q$ being true does not, by itself, ensure that $Q$ is true, because there is one case (c) in which $P \to Q$ is true, but $Q$ is false. However, with the additional requirement that $P$ is true, we are restricted to the case (a) in which $Q$ is also true. Thus, if the premises to modus ponens are true, then so is its conclusion.
Now, it's worth considering how this applies to the example that you gave. The example of “all men are mortal, Socrates is man, therefore Socrates is mortal”. It uses first-order reasoning, and is not actually a case of modus ponens, neither premise is a conditional. However, the proof does use _modus ponens_, in that it requires us to make the following inference.
There are two important concepts to consider: soundness and validity. These mean slightly different things for inference rules and for arguments.
An inference rule is sound if whenever its premises are true, then its conclusion is true. As we saw earlier, modus ponens is a sound rule of inference. The term valid is not used concerning inference rules. We do not say that an inference rule is valid or invalid.
An argument is valid if each reasoning step is an application of a sound inference rule. This means that each sentence in the argument must be true if the earlier sentences that it is based on are true. It does not make the claim that those earlier sentence are true, but just that if they are true, then the current sentence is true. An argument is sound if its premises are, in fact, true. If an argument is both sound and valid, then its conclusion must be true.
So, both
and
are valid arguments, because they use only valid inference rules (namely, modus ponens). The first argument is sound because both of its premises are true. The second argument is unsound because one of its premises its second premise, “Italy is man,” is not true.
If the conclusion of an argument is not true, it means that the argument is either invalid or unsound. (Of course, it could also be both.)