Equality is Transitive

Theorem

$\forall a, b, c: \paren {a = b} \land \paren {b = c} \implies a = c$

Proof

 $\ds a$ $=$ $\ds b$ $\ds \vdash \ \$ $\ds \map P a$ $\iff$ $\ds \map P b$ Leibniz's law $\ds b$ $=$ $\ds c$ $\ds \vdash \ \$ $\ds \map P b$ $\iff$ $\ds \map P c$ Leibniz's law $\ds \vdash \ \$ $\ds \map P a$ $\iff$ $\ds \map P c$ Biconditional is Transitive $\ds \vdash \ \$ $\ds a$ $=$ $\ds c$ Leibniz's law

$\blacksquare$