Formal deduction proof of predicates

Question

I am trying to proof equality is transitive, that is,

$\emptyset \vdash \forall x \forall y \forall z ((x=y) \land (y=z) \to(x=z))$

using formal deduction (17 rules) and also other rules (ex.

To begin, I thought of using $\to$elimination to get the 2 separate clauses

$\sum \vdash(x=y) \land (y=z)$

$\sum \vdash(x=z)$

and then using $\land$elimination to further simplify it to

$\sum \vdash(x=y),(y=z)$

but I am not sure of how to proceed from this step. Does anyone know how to solve this? Thanks in advance!

17 rules:

Answer 1

1) $x=y \vdash x=y$ --- Rule 1

2) $\vdash x=x$ --- $=$-intro

3) $x=y \vdash y=x$ --- from 1) and 2) by $=$-elim, with $A(x) := y=x$

4) $x=y, y=z \vdash y=x$ --- from 3) by Rule 2

5) $x=y, y=z \vdash y=z$ --- Rules 1 and 2

6) $x=y, y=z \vdash x=z$ --- from 4) and 5) by $=$-elim, with $A(y) := y=z$.