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

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