Metamath Proof Explorer


Theorem ot21std

Description: Extract the first member of an ordered triple. Deduction version. (Contributed by Scott Fenton, 21-Aug-2024)

Ref Expression
Hypotheses ot21st.1 A V
ot21st.2 B V
ot21st.3 C V
Assertion ot21std X = A B C 1 st 1 st X = A

Proof

Step Hyp Ref Expression
1 ot21st.1 A V
2 ot21st.2 B V
3 ot21st.3 C V
4 opex A B V
5 4 3 op1std X = A B C 1 st X = A B
6 5 fveq2d X = A B C 1 st 1 st X = 1 st A B
7 1 2 op1st 1 st A B = A
8 6 7 eqtrdi X = A B C 1 st 1 st X = A