Theorem tpeq123d

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

	Ref	Expression
Hypotheses	tpeq1d.1	|- ( ph -> A = B )
	tpeq123d.2	|- ( ph -> C = D )
	tpeq123d.3	|- ( ph -> E = F )
Assertion	tpeq123d	|- ( ph -> { A , C , E } = { B , D , F } )

Proof

Step	Hyp	Ref	Expression
1		tpeq1d.1	|- ( ph -> A = B )
2		tpeq123d.2	|- ( ph -> C = D )
3		tpeq123d.3	|- ( ph -> E = F )
4	1	tpeq1d	|- ( ph -> { A , C , E } = { B , C , E } )
5	2	tpeq2d	|- ( ph -> { B , C , E } = { B , D , E } )
6	3	tpeq3d	|- ( ph -> { B , D , E } = { B , D , F } )
7	4 5 6	3eqtrd	|- ( ph -> { A , C , E } = { B , D , F } )