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

Metamath Proof Explorer

Theorem tprot

Description: Rotation of the elements of an unordered triple. (Contributed by Alan Sare, 24-Oct-2011)

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

Proof

Step Hyp Ref Expression
1 3orrot ⊢ x = A ∨ x = B ∨ x = C ↔ x = B ∨ x = C ∨ x = A
2 1 abbii ⊢ x | x = A ∨ x = B ∨ x = C = x | x = B ∨ x = C ∨ x = A
3 dftp2 ⊢ A B C = x | x = A ∨ x = B ∨ x = C
4 dftp2 ⊢ B C A = x | x = B ∨ x = C ∨ x = A
5 2 3 4 3eqtr4i ⊢ A B C = B C A