Formal deduction proof of predicates 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:

 A: 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$.

A: Here is one way to show this. I am using a Fitch-style proof checker to make sure I am following the rules.

On the first line I assume the names, $a$, $b$ and $c$, have the identity relationships specified by the antecedent of the conditional I want to derive. 
On line 4, I use identity elimination (=E). See chapter 24 of the forallx text for a discussion of identity. Given line 2, $a$ can be substituted for $b$. That substitution is used in line 3 to derive line 4.
Conditional introduction occurs on line 5 which discharges the assumption on line 1. After that each of the universally quantified variables are introduced to reach the goal.

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/
P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Fall 2019. http://forallx.openlogicproject.org/forallxyyc.pdf
