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

Metamath Proof Explorer

Theorem tpcomb

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

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

Proof

Step Hyp Ref Expression
1 tpcoma ⊢ B C A = C B A
2 tprot ⊢ A B C = B C A
3 tprot ⊢ A C B = C B A
4 1 2 3 3eqtr4i ⊢ A B C = A C B