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

Metamath Proof Explorer

Theorem tpidm

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

Ref Expression
Assertion tpidm ⊢ A A A = A

Proof

Step Hyp Ref Expression
1 tpidm12 ⊢ A A A = A A
2 dfsn2 ⊢ A = A A
3 1 2 eqtr4i ⊢ A A A = A