Theorem tpcomb

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

	Ref	Expression
Assertion	tpcomb	⊢ { 𝐴 , 𝐵 , 𝐶 } = { 𝐴 , 𝐶 , 𝐵 }

Proof

Step	Hyp	Ref	Expression
1		tpcoma	⊢ { 𝐵 , 𝐶 , 𝐴 } = { 𝐶 , 𝐵 , 𝐴 }
2		tprot	⊢ { 𝐴 , 𝐵 , 𝐶 } = { 𝐵 , 𝐶 , 𝐴 }
3		tprot	⊢ { 𝐴 , 𝐶 , 𝐵 } = { 𝐶 , 𝐵 , 𝐴 }
4	1 2 3	3eqtr4i	⊢ { 𝐴 , 𝐵 , 𝐶 } = { 𝐴 , 𝐶 , 𝐵 }