Metamath Proof Explorer


Theorem sub32

Description: Swap the second and third terms in a double subtraction. (Contributed by NM, 19-Aug-2005)

Ref Expression
Assertion sub32 ABCA-B-C=A-C-B

Proof

Step Hyp Ref Expression
1 addcom BCB+C=C+B
2 1 3adant1 ABCB+C=C+B
3 2 oveq2d ABCAB+C=AC+B
4 subsub4 ABCA-B-C=AB+C
5 subsub4 ACBA-C-B=AC+B
6 5 3com23 ABCA-C-B=AC+B
7 3 4 6 3eqtr4d ABCA-B-C=A-C-B