Description: Extract the first member of an ordered triple. Deduction version. (Contributed by Scott Fenton, 21-Aug-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ot21st.1 | ||
ot21st.2 | |||
ot21st.3 | |||
Assertion | ot21std |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ot21st.1 | ||
2 | ot21st.2 | ||
3 | ot21st.3 | ||
4 | opex | ||
5 | 4 3 | op1std | |
6 | 5 | fveq2d | |
7 | 1 2 | op1st | |
8 | 6 7 | eqtrdi |