Theorem tpeq123d

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

	Ref	Expression
Hypotheses	tpeq1d.1	⊢ ( 𝜑 → 𝐴 = 𝐵 )
	tpeq123d.2	⊢ ( 𝜑 → 𝐶 = 𝐷 )
	tpeq123d.3	⊢ ( 𝜑 → 𝐸 = 𝐹 )
Assertion	tpeq123d	⊢ ( 𝜑 → { 𝐴 , 𝐶 , 𝐸 } = { 𝐵 , 𝐷 , 𝐹 } )

Proof

Step	Hyp	Ref	Expression
1		tpeq1d.1	⊢ ( 𝜑 → 𝐴 = 𝐵 )
2		tpeq123d.2	⊢ ( 𝜑 → 𝐶 = 𝐷 )
3		tpeq123d.3	⊢ ( 𝜑 → 𝐸 = 𝐹 )
4	1	tpeq1d	⊢ ( 𝜑 → { 𝐴 , 𝐶 , 𝐸 } = { 𝐵 , 𝐶 , 𝐸 } )
5	2	tpeq2d	⊢ ( 𝜑 → { 𝐵 , 𝐶 , 𝐸 } = { 𝐵 , 𝐷 , 𝐸 } )
6	3	tpeq3d	⊢ ( 𝜑 → { 𝐵 , 𝐷 , 𝐸 } = { 𝐵 , 𝐷 , 𝐹 } )
7	4 5 6	3eqtrd	⊢ ( 𝜑 → { 𝐴 , 𝐶 , 𝐸 } = { 𝐵 , 𝐷 , 𝐹 } )