What are the relations and differences between Implication, inference rule and equivalence in logic? In first order predicate logic, implication is an operator on formulas

If $φ$ and $ψ$ are formulas, then $φ  \rightarrow ψ$ is a formula.

We also have that if formulas $P_1$ implies $P_2$  and  $P_2$ implies $P_3$, then  $P_1$ implies $P_3$, i.e.,
1  → 2 
2  → 3
---------
1  → 3

Is the above considered as a inference rule? or a formula (1  → 2) ∧ (2  → 3)  → (1  → 3)? Why is it considered as one but not the other?
We also have that
(P1 → P2) ≡ ( ¬P1 ∨ P 2)
(¬∃X [P(X)]) ≡ (∀X [ ¬P(X)])
¬ (P1 ∧ P2) ≡ (¬P1 ∨ ¬P2)

Are the above three considered as three formulas, or as some equivalence relation between formulas? Why are they considered as one but not the other?
Thanks.
 A: 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. 
