Metamath Proof Explorer


Theorem tpidm13

Description: Unordered triple { A , B , A } is just an overlong way to write { A , B } . (Contributed by David A. Wheeler, 10-May-2015)

Ref Expression
Assertion tpidm13 ABA=AB

Proof

Step Hyp Ref Expression
1 tprot AAB=ABA
2 tpidm12 AAB=AB
3 1 2 eqtr3i ABA=AB