Metamath Proof Explorer


Theorem oteq3

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

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

Proof

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