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

Metamath Proof Explorer

Theorem tpcoma

Description: Swap 1st and 2nd members of an unordered triple. (Contributed by NM, 22-May-2015)

Ref Expression
Assertion tpcoma ⊢ A B C = B A C

Proof

Step Hyp Ref Expression
1 prcom ⊢ A B = B A
2 1 uneq1i ⊢ A B ∪ C = B A ∪ C
3 df-tp ⊢ A B C = A B ∪ C
4 df-tp ⊢ B A C = B A ∪ C
5 2 3 4 3eqtr4i ⊢ A B C = B A C