Theorem oteq123d

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

	Ref	Expression
Hypotheses	oteq1d.1	|- ( ph -> A = B )
	oteq123d.2	|- ( ph -> C = D )
	oteq123d.3	|- ( ph -> E = F )
Assertion	oteq123d	|- ( ph -> <. A , C , E >. = <. B , D , F >. )

Proof

Step	Hyp	Ref	Expression
1		oteq1d.1	|- ( ph -> A = B )
2		oteq123d.2	|- ( ph -> C = D )
3		oteq123d.3	|- ( ph -> E = F )
4	1	oteq1d	|- ( ph -> <. A , C , E >. = <. B , C , E >. )
5	2	oteq2d	|- ( ph -> <. B , C , E >. = <. B , D , E >. )
6	3	oteq3d	|- ( ph -> <. B , D , E >. = <. B , D , F >. )
7	4 5 6	3eqtrd	|- ( ph -> <. A , C , E >. = <. B , D , F >. )