Metamath Proof Explorer


Theorem tppreq3

Description: An unordered triple is an unordered pair if one of its elements is identical with another element. (Contributed by Alexander van der Vekens, 6-Oct-2017)

Ref Expression
Assertion tppreq3 B = C A B C = A B

Proof

Step Hyp Ref Expression
1 tpeq3 C = B A B C = A B B
2 1 eqcoms B = C A B C = A B B
3 tpidm23 A B B = A B
4 2 3 eqtrdi B = C A B C = A B