About the Axiom of Quantifier Introduction, in your quotation you have forgot the proviso.
The complete formulation is:
$\vdash (\varphi → ∀x \varphi)$, if $x$ is not [free] in $\varphi$.
This formula is valid and the proviso does not licence the derivation of the invalid : $(Px \rightarrow \forall xPx)$.
The proviso is also the reason why this axiom and the Rule of Modus Ponens are not enough to derive the Rule of Generalization.
With them we can only derive a "restricted version" of it :
If $\vdash \varphi$ and $x$ is not free in $\varphi$, then $\vdash \forall x \varphi$.
This axiom can be used in connection with another quantifier axiom : the Axiom of Quantified Implication, to prove the :
GENERALIZATION (meta-)THEOREM : If $\Gamma \vdash \varphi$ and $x$ does not occur free in any formula in $\Gamma$, then $\Gamma \vdash \forall x \varphi$.
From it, with $\Gamma = \emptyset$ [there are no formulae in $\Gamma$: thus, the proviso is vacuously satisfied], we can derive the (unrestricted) Rule of Generalization :
If $\vdash \varphi$, then $\vdash \forall x \varphi$.
if $\vdash P$, then $\vdash Q$
$\vdash (P \rightarrow Q)$
there is a difference : the two are not equivalent.
Consider propositional logic; if we have derived : $P \rightarrow Q$ and $P$, it is enough to apply modus ponens to derive : $Q$.
But from the assumption : if $\vdash P$, then $\vdash Q$, does not follows that : $\vdash (P \rightarrow Q)$.
It is well known that, if $p_1$ is a sentential letter, we cannot have $\vdash p_1$ (no sentential letter is a tautology); of course, the same holds with $\vdash \lnot p_1$. Thus, both $\vdash p_1$ and $\vdash \lnot p_1$ are false (meta-)logical assertions.
Then, the conditional : "if $\vdash p_1$, then $\vdash \lnot p_1$" is true.
But of course, $\nvdash p_1 \rightarrow \lnot p_1$ ($p_1 \rightarrow \lnot p_1$ is not a tautology).
See Jan von Plato, Elements of Logical Reasoning (2013), page 47 :
The "argument" :
Assume that if $P$ is derivable, then $Q$ is. Then $P \rightarrow Q$ is derivable
is a logical fallacy.
These considerations apply also to Generalization : we have "if $\vdash \varphi$, then $\vdash \forall x \varphi$" (it is the Rule of Generalization.) but not (without proviso) $\vdash (\varphi \rightarrow \forall x \varphi)$.