Metamath Proof Explorer


Theorem tpid2

Description: One of the three elements of an unordered triple. (Contributed by NM, 7-Apr-1994) (Proof shortened by Andrew Salmon, 29-Jun-2011)

Ref Expression
Hypothesis tpid2.1 B V
Assertion tpid2 B A B C

Proof

Step Hyp Ref Expression
1 tpid2.1 B V
2 eqid B = B
3 2 3mix2i B = A B = B B = C
4 1 eltp B A B C B = A B = B B = C
5 3 4 mpbir B A B C