This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sub31

Description: Swap the first and third terms in a double subtraction. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion sub31 
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A - ( B - C ) ) = ( C - ( B - A ) ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> A e. CC )
2 simpr 
 |-  ( ( B e. CC /\ C e. CC ) -> C e. CC )
3 simpl 
 |-  ( ( B e. CC /\ C e. CC ) -> B e. CC )
4 2 3 subcld 
 |-  ( ( B e. CC /\ C e. CC ) -> ( C - B ) e. CC )
5 4 3adant1 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( C - B ) e. CC )
6 1 5 addcomd 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A + ( C - B ) ) = ( ( C - B ) + A ) )
7 subsub2 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A - ( B - C ) ) = ( A + ( C - B ) ) )
8 simp3 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> C e. CC )
9 simp2 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> B e. CC )
10 8 9 1 subsubd 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( C - ( B - A ) ) = ( ( C - B ) + A ) )
11 6 7 10 3eqtr4d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A - ( B - C ) ) = ( C - ( B - A ) ) )