# Metamath Proof Explorer

## Theorem ot2ndg

Description: Extract the second member of an ordered triple. (See ot1stg comment.) (Contributed by NM, 3-Apr-2015) (Revised by Mario Carneiro, 2-May-2015)

Ref Expression
Assertion ot2ndg ${⊢}\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\to {2}^{nd}\left({1}^{st}\left(⟨{A},{B},{C}⟩\right)\right)={B}$

### Proof

Step Hyp Ref Expression
1 df-ot ${⊢}⟨{A},{B},{C}⟩=⟨⟨{A},{B}⟩,{C}⟩$
2 1 fveq2i ${⊢}{1}^{st}\left(⟨{A},{B},{C}⟩\right)={1}^{st}\left(⟨⟨{A},{B}⟩,{C}⟩\right)$
3 opex ${⊢}⟨{A},{B}⟩\in \mathrm{V}$
4 op1stg ${⊢}\left(⟨{A},{B}⟩\in \mathrm{V}\wedge {C}\in {X}\right)\to {1}^{st}\left(⟨⟨{A},{B}⟩,{C}⟩\right)=⟨{A},{B}⟩$
5 3 4 mpan ${⊢}{C}\in {X}\to {1}^{st}\left(⟨⟨{A},{B}⟩,{C}⟩\right)=⟨{A},{B}⟩$
6 2 5 syl5eq ${⊢}{C}\in {X}\to {1}^{st}\left(⟨{A},{B},{C}⟩\right)=⟨{A},{B}⟩$
7 6 fveq2d ${⊢}{C}\in {X}\to {2}^{nd}\left({1}^{st}\left(⟨{A},{B},{C}⟩\right)\right)={2}^{nd}\left(⟨{A},{B}⟩\right)$
8 op2ndg ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to {2}^{nd}\left(⟨{A},{B}⟩\right)={B}$
9 7 8 sylan9eqr ${⊢}\left(\left({A}\in {V}\wedge {B}\in {W}\right)\wedge {C}\in {X}\right)\to {2}^{nd}\left({1}^{st}\left(⟨{A},{B},{C}⟩\right)\right)={B}$
10 9 3impa ${⊢}\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\to {2}^{nd}\left({1}^{st}\left(⟨{A},{B},{C}⟩\right)\right)={B}$