Help understanding $x=y\Rightarrow(x=z\Rightarrow y=z)$ I was reading a proof that opened with the integer axiom of $x=y\Rightarrow(x=z\Rightarrow y=z)$
What would be an accurate statement in English to express this?  The "implies" within the first "implies" is kind of confusing to me.  I believe the general idea is that if $x$ equals $y$, then if $x$ equals $z$, $y$ also equals $z$.
 A: If $x$ is equal to $y$, then anything equal to $x$ must also be equal to $y$.
A: "If z is the same thing as x, and y is the same thing as x, then z is the same thing as y."
A: In general, you can use the word "that" to describe implication of implications:
$x=y$ implies that $x=z$ implies $y=z$.
"p implies q" implies $that$ if not q then not p.
$(p \implies q) \implies (\neg q \implies \neg p)$
A: (Perhaps not a direct answer to your question, but this might be helpful.)
In my opinion this is most easily understood as a specific instance of
$$(0) \;\;\; x = y \;\Rightarrow\; (P(x) \Rightarrow P(y))$$
where $\;P(\cdot)\;$ is any boolean expression of one variable.  And in turn this is a weaker form of
$$(1) \;\;\; x = y \;\Rightarrow\; (P(x) \equiv P(y))$$
which Dijkstra calls Leibniz' rule, and which the Wikipedia page on the topic calls "The indiscernibility of identicals".
Now $(1)$ in plain English: "If $\;x\;$ equals $\;y\;$, then whatever is true of $\;x\;$ is true of $\;y\;$, and vice versa."  (If you leave out the "and vice versa" part, of course you get $(0)$.)
A: if (x,y)ϵf and (x,z)ϵf  → y=z.
https://en.wikipedia.org/wiki/Transitive_relation
