Metamath Proof Explorer


Theorem tpid1

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 tpid1.1 A V
Assertion tpid1 A A B C

Proof

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