Metamath Proof Explorer


Theorem un12

Description: A rearrangement of union. (Contributed by NM, 12-Aug-2004)

Ref Expression
Assertion un12 ABC=BAC

Proof

Step Hyp Ref Expression
1 uncom AB=BA
2 1 uneq1i ABC=BAC
3 unass ABC=ABC
4 unass BAC=BAC
5 2 3 4 3eqtr3i ABC=BAC