This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∈ V → 2 nd ⁡ A B C = C

Proof

Step Hyp Ref Expression
1 df-ot ⊢ A B C = A B C
2 1 fveq2i ⊢ 2 nd ⁡ A B C = 2 nd ⁡ A B C
3 opex ⊢ A B ∈ V
4 op2ndg ⊢ A B ∈ V ∧ C ∈ V → 2 nd ⁡ A B C = C
5 3 4 mpan ⊢ C ∈ V → 2 nd ⁡ A B C = C
6 2 5 eqtrid ⊢ C ∈ V → 2 nd ⁡ A B C = C