Theorem sub31

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

	Ref	Expression
Assertion	sub31	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 − ( 𝐵 − 𝐶 ) ) = ( 𝐶 − ( 𝐵 − 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐴 ∈ ℂ )
2		simpr	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐶 ∈ ℂ )
3		simpl	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐵 ∈ ℂ )
4	2 3	subcld	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐶 − 𝐵 ) ∈ ℂ )
5	4	3adant1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐶 − 𝐵 ) ∈ ℂ )
6	1 5	addcomd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 + ( 𝐶 − 𝐵 ) ) = ( ( 𝐶 − 𝐵 ) + 𝐴 ) )
7		subsub2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 − ( 𝐵 − 𝐶 ) ) = ( 𝐴 + ( 𝐶 − 𝐵 ) ) )
8		simp3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐶 ∈ ℂ )
9		simp2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐵 ∈ ℂ )
10	8 9 1	subsubd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐶 − ( 𝐵 − 𝐴 ) ) = ( ( 𝐶 − 𝐵 ) + 𝐴 ) )
11	6 7 10	3eqtr4d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 − ( 𝐵 − 𝐶 ) ) = ( 𝐶 − ( 𝐵 − 𝐴 ) ) )