Theorem ot3rdg

Description: Extract the third member of an ordered triple. (See ot1stg comment.) (Contributed by NM, 3-Apr-2015)

	Ref	Expression
Assertion	ot3rdg	$$⊢C\in V\to 2^{nd}\left(⟨A,B,C⟩\right)=C$$

Proof

Step	Hyp	Ref	Expression
1		df-ot	$$⊢⟨A,B,C⟩=⟨⟨A,B⟩,C⟩$$
2	1	fveq2i	$$⊢2^{nd}\left(⟨A,B,C⟩\right)=2^{nd}\left(⟨⟨A,B⟩,C⟩\right)$$
3		opex	$$⊢⟨A,B⟩\in \mathrm{V}$$
4		op2ndg	$$⊢\left(⟨A,B⟩\in \mathrm{V}\wedge C\in V\right)\to 2^{nd}\left(⟨⟨A,B⟩,C⟩\right)=C$$
5	3 4	mpan	$$⊢C\in V\to 2^{nd}\left(⟨⟨A,B⟩,C⟩\right)=C$$
6	2 5	eqtrid	$$⊢C\in V\to 2^{nd}\left(⟨A,B,C⟩\right)=C$$