Theorem oteq2

Description: Equality theorem for ordered triples. (Contributed by NM, 3-Apr-2015)

	Ref	Expression
Assertion	oteq2	|- ( A = B -> <. C , A , D >. = <. C , B , D >. )

Proof

Step	Hyp	Ref	Expression
1		opeq2	|- ( A = B -> <. C , A >. = <. C , B >. )
2	1	opeq1d	|- ( A = B -> <. <. C , A >. , D >. = <. <. C , B >. , D >. )
3		df-ot	|- <. C , A , D >. = <. <. C , A >. , D >.
4		df-ot	|- <. C , B , D >. = <. <. C , B >. , D >.
5	2 3 4	3eqtr4g	|- ( A = B -> <. C , A , D >. = <. C , B , D >. )