Metamath Proof Explorer


Theorem oteqimp

Description: The components of an ordered triple. (Contributed by Alexander van der Vekens, 2-Mar-2018)

Ref Expression
Assertion oteqimp T = A B C A X B Y C Z 1 st 1 st T = A 2 nd 1 st T = B 2 nd T = C

Proof

Step Hyp Ref Expression
1 ot1stg A X B Y C Z 1 st 1 st A B C = A
2 ot2ndg A X B Y C Z 2 nd 1 st A B C = B
3 ot3rdg C Z 2 nd A B C = C
4 3 3ad2ant3 A X B Y C Z 2 nd A B C = C
5 1 2 4 3jca A X B Y C Z 1 st 1 st A B C = A 2 nd 1 st A B C = B 2 nd A B C = C
6 2fveq3 T = A B C 1 st 1 st T = 1 st 1 st A B C
7 6 eqeq1d T = A B C 1 st 1 st T = A 1 st 1 st A B C = A
8 2fveq3 T = A B C 2 nd 1 st T = 2 nd 1 st A B C
9 8 eqeq1d T = A B C 2 nd 1 st T = B 2 nd 1 st A B C = B
10 fveqeq2 T = A B C 2 nd T = C 2 nd A B C = C
11 7 9 10 3anbi123d T = A B C 1 st 1 st T = A 2 nd 1 st T = B 2 nd T = C 1 st 1 st A B C = A 2 nd 1 st A B C = B 2 nd A B C = C
12 5 11 syl5ibr T = A B C A X B Y C Z 1 st 1 st T = A 2 nd 1 st T = B 2 nd T = C