Theorem tpeq123d

Description: Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014)

	Ref	Expression
Hypotheses	tpeq1d.1	$$⊢\phi \to A=B$$
	tpeq123d.2	$$⊢\phi \to C=D$$
	tpeq123d.3	$$⊢\phi \to E=F$$
Assertion	tpeq123d	$$⊢\phi \to \left\{A,C,E\right\}=\left\{B,D,F\right\}$$

Proof

Step	Hyp	Ref	Expression
1		tpeq1d.1	$$⊢\phi \to A=B$$
2		tpeq123d.2	$$⊢\phi \to C=D$$
3		tpeq123d.3	$$⊢\phi \to E=F$$
4	1	tpeq1d	$$⊢\phi \to \left\{A,C,E\right\}=\left\{B,C,E\right\}$$
5	2	tpeq2d	$$⊢\phi \to \left\{B,C,E\right\}=\left\{B,D,E\right\}$$
6	3	tpeq3d	$$⊢\phi \to \left\{B,D,E\right\}=\left\{B,D,F\right\}$$
7	4 5 6	3eqtrd	$$⊢\phi \to \left\{A,C,E\right\}=\left\{B,D,F\right\}$$