Metamath Proof Explorer


Theorem dif32

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

Ref Expression
Assertion dif32 ABC=ACB

Proof

Step Hyp Ref Expression
1 uncom BC=CB
2 1 difeq2i ABC=ACB
3 difun1 ABC=ABC
4 difun1 ACB=ACB
5 2 3 4 3eqtr3i ABC=ACB