Metamath Proof Explorer


Theorem tpass

Description: Split off the first element of an unordered triple. (Contributed by Mario Carneiro, 5-Jan-2016)

Ref Expression
Assertion tpass ABC=ABC

Proof

Step Hyp Ref Expression
1 df-tp BCA=BCA
2 tprot ABC=BCA
3 uncom ABC=BCA
4 1 2 3 3eqtr4i ABC=ABC