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

\(\displaystyle a\) \(=\) \(\displaystyle b\)
\(\displaystyle \vdash \ \ \) \(\displaystyle \map P a\) \(\iff\) \(\displaystyle \map P b\) Leibniz's law
\(\displaystyle b\) \(=\) \(\displaystyle c\)
\(\displaystyle \vdash \ \ \) \(\displaystyle \map P b\) \(\iff\) \(\displaystyle \map P c\) Leibniz's law
\(\displaystyle \vdash \ \ \) \(\displaystyle \map P a\) \(\iff\) \(\displaystyle \map P c\) Biconditional is Transitive
\(\displaystyle \vdash \ \ \) \(\displaystyle a\) \(=\) \(\displaystyle c\) Leibniz's law

$\blacksquare$


Sources