First Order Logic: how to prove the formula?

Question

How to show this formula using axioms of First Order Logic: $\forall x_{0}, \forall x_{1}, \forall x_2 ((x_{0}=x_{1})\wedge (P(x_1,x_2) \rightarrow Q(x_1,x_2) )\rightarrow (P(x_0,x_2) \rightarrow Q(x_0,x_2)))$?

$\textbf{My work}:$

1) $\forall x_{0}, \forall x_{1}, \forall x_2 ((x_{0}=x_{1})\wedge P(x_1,x_2) \rightarrow P(x_0,x_1))$ - axiom of equality

2) $\forall x_{0}, \forall x_{1}, \forall x_2 ((x_{0}=x_{1})\wedge P(x_1,x_2) \rightarrow P(x_0,x_1)) \rightarrow\forall x_{1}, \forall x_2 ((x_{0}=x_{1})\wedge P(x_1,x_2) \rightarrow P(x_0,x_1))$ - axiom

3)$\forall x_{1}, \forall x_2 ((x_{0}=x_{1})\wedge P(x_1,x_2) \rightarrow P(x_0,x_1))$ - MP(1,2)

4) 2 times I repeat similar steps like in 1), 2), 3) and get $(x_{0}=x_{1})\wedge P(x_1,x_2) \rightarrow P(x_0,x_1)$

5) With $Q$ I do the same thing and get $(x_{0}=x_{1})\wedge Q(x_1,x_2) \rightarrow Q(x_0,x_1)$.

I dont know what to do next...

Answer 1

Hint

The formula :

$∀x_0,∀x_1,∀x_2((x_0=x_1) ∧ (P(x_1,x_2) → Q(x_1,x_2)) → (P(x_0,x_2) → Q(x_0,x_2)))$

is a simple "variant" of the substitution axiom for equality :

$\vdash ( x = y) \to (\phi[z:=x] \to \phi[z:=y])$

where $\phi(z)$ is : $P(z,x_2) → Q(z,x_2)$.

Thus, we have to start from $(x_0=x_1)$ and with equality axioms derive : $(x_1=x_0)$.

Then apply the above axiom schema to get :

$(x_0=x_1) \vdash (P(x_1,x_2) → Q(x_1,x_2)) → (P(x_0,x_2) → Q(x_0,x_2)))$.

Finally, we have to use the Deduction Theorem followed by Generalization thrice.