Rule T in First-Order Logic

Question

In Enderton's A Mathematical Introduction to Logic (second edition, page 118), we are given the so-called Rule T (Lemma $24C$) :

If $\Gamma\vdash\alpha_1,\ldots,\Gamma\vdash\alpha_n$ and $\left\{\alpha_1,\ldots,\alpha_n\right\}$ tautologically implies $\beta$, then $\Gamma\vdash\beta$.

Conceptually, this is fine. However, I don't quite see how/why it is used in the following example:

Show that $\vdash\forall x\forall y(x=y\to y=x)$:

1. $\vdash x=y\to (x=x\to y=x)\qquad\text{(Axiom 6)}$
2. $\vdash x=x\qquad\qquad\qquad\qquad\qquad\quad\text{(Axiom 5)}$
3. $\vdash x=y\to y=x\qquad\qquad\qquad\quad\text{(Rule T)}$
4. $\vdash \forall y(x=y\to y=x)\qquad\qquad\quad\text{(Generalization Theorem)}$
5. $\vdash \forall x\forall y(x=y\to y=x)\qquad\qquad\text{(Generalization Theorem)}$

Furthermore, from the definition given above, if we already have $\Gamma\vdash\alpha_1,\ldots,\Gamma\vdash\alpha_n$ and $\Gamma\vdash\alpha_1\to\ldots\to\alpha_n\to\beta$ (since this is a tautology), then how is Rule T different from $n$ applications of Modus Ponens? Or is it precisely that?

Answer 1

We have to apply Rule T with $\Gamma = \emptyset$ and using the tautological implication :

$A \to (B \to C) \vDash B \to (A \to C)$

where $B$ is $x=x$.

In this way, from 1, we get :

1'. $ \ \vdash x=x \to (x=y \to y=x)$

and with 2. we can derive 3. by modus ponens.