Theorem oteq1

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

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

Proof

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