Equality is Transitive

From ProofWiki

Jump to: navigation, search

Theorem

That is:

$\forall a, b, c: \left({a = b}\right) \land \left({b = c}\right) \implies a = c$

$\displaystyle $	$\displaystyle $	$\displaystyle $	$\displaystyle a$	$=$	$\displaystyle b$	$\displaystyle $	$\displaystyle $	$\displaystyle $
$\displaystyle $	$\displaystyle \vdash$	$\displaystyle $	$\displaystyle P \ \left({a}\right)$	$\iff$	$\displaystyle P \ \left({b}\right)$	$\displaystyle $	$\displaystyle $	$\displaystyle $	Leibniz's Law
$\displaystyle $	$\displaystyle $	$\displaystyle $	$\displaystyle b$	$=$	$\displaystyle c$	$\displaystyle $	$\displaystyle $	$\displaystyle $
$\displaystyle $	$\displaystyle \vdash$	$\displaystyle $	$\displaystyle P \ \left({b}\right)$	$\iff$	$\displaystyle P \ \left({c}\right)$	$\displaystyle $	$\displaystyle $	$\displaystyle $	Leibniz's Law
$\displaystyle $	$\displaystyle \vdash$	$\displaystyle $	$\displaystyle P \ \left({a}\right)$	$\iff$	$\displaystyle P \ \left({c}\right)$	$\displaystyle $	$\displaystyle $	$\displaystyle $	Biconditional is Transitive
$\displaystyle $	$\displaystyle \vdash$	$\displaystyle $	$\displaystyle a$	$=$	$\displaystyle c$	$\displaystyle $	$\displaystyle $	$\displaystyle $	Leibniz's Law

$\blacksquare$

\(\displaystyle \)	\(\displaystyle \)	\(\displaystyle \)	\(\displaystyle a\)	\(=\)	\(\displaystyle b\)	\(\displaystyle \)	\(\displaystyle \)	\(\displaystyle \)
\(\displaystyle \)	\(\displaystyle \vdash\)	\(\displaystyle \)	\(\displaystyle P \ \left({a}\right)\)	\(\iff\)	\(\displaystyle P \ \left({b}\right)\)	\(\displaystyle \)	\(\displaystyle \)	\(\displaystyle \)	Leibniz's Law
\(\displaystyle \)	\(\displaystyle \)	\(\displaystyle \)	\(\displaystyle b\)	\(=\)	\(\displaystyle c\)	\(\displaystyle \)	\(\displaystyle \)	\(\displaystyle \)
\(\displaystyle \)	\(\displaystyle \vdash\)	\(\displaystyle \)	\(\displaystyle P \ \left({b}\right)\)	\(\iff\)	\(\displaystyle P \ \left({c}\right)\)	\(\displaystyle \)	\(\displaystyle \)	\(\displaystyle \)	Leibniz's Law
\(\displaystyle \)	\(\displaystyle \vdash\)	\(\displaystyle \)	\(\displaystyle P \ \left({a}\right)\)	\(\iff\)	\(\displaystyle P \ \left({c}\right)\)	\(\displaystyle \)	\(\displaystyle \)	\(\displaystyle \)	Biconditional is Transitive
\(\displaystyle \)	\(\displaystyle \vdash\)	\(\displaystyle \)	\(\displaystyle a\)	\(=\)	\(\displaystyle c\)	\(\displaystyle \)	\(\displaystyle \)	\(\displaystyle \)	Leibniz's Law