Metamath Proof Explorer


Theorem dif32

Description: Swap second and third argument of double difference. (Contributed by NM, 18-Aug-2004)

Ref Expression
Assertion dif32 A B C = A C B

Proof

Step Hyp Ref Expression
1 uncom B C = C B
2 1 difeq2i A B C = A C B
3 difun1 A B C = A B C
4 difun1 A C B = A C B
5 2 3 4 3eqtr3i A B C = A C B