Theorem oteq123d

Description: Equality deduction for ordered triples. (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypotheses	oteq1d.1	$$⊢\phi \to A=B$$
	oteq123d.2	$$⊢\phi \to C=D$$
	oteq123d.3	$$⊢\phi \to E=F$$
Assertion	oteq123d	$$⊢\phi \to ⟨A,C,E⟩=⟨B,D,F⟩$$

Proof

Step	Hyp	Ref	Expression
1		oteq1d.1	$$⊢\phi \to A=B$$
2		oteq123d.2	$$⊢\phi \to C=D$$
3		oteq123d.3	$$⊢\phi \to E=F$$
4	1	oteq1d	$$⊢\phi \to ⟨A,C,E⟩=⟨B,C,E⟩$$
5	2	oteq2d	$$⊢\phi \to ⟨B,C,E⟩=⟨B,D,E⟩$$
6	3	oteq3d	$$⊢\phi \to ⟨B,D,E⟩=⟨B,D,F⟩$$
7	4 5 6	3eqtrd	$$⊢\phi \to ⟨A,C,E⟩=⟨B,D,F⟩$$