Description: Equality theorem for ordered triples. (Contributed by NM, 3-Apr-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | oteq3 | |- ( A = B -> <. C , D , A >. = <. C , D , B >. ) |
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 >. ) |