Equality is Transitive

From ProofWiki
Jump to navigation Jump to search

Theorem

Equality is transitive:

$\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$


Also see


Sources